Two mods suggested by Jared Davis: fixed a bug in pons-addr-of-argument, and added three arithmetic theorems to axioms.lisp.  Technical mod: fixed (getprop nil 'absolute-event-number ...).

Quoting :doc note-7-0:

  Three new theorems were added to the ACL2 build to allow some
  additional simple arithmetic reasoning. For example, the following
  failed before this change, typically causing the user to include an
  arithmetic book; but that is no longer necessary.

    (thm (implies (natp x)
                  (equal (expt 2 (+ 1 -1 x))
                         (expt 2 x))))

  Thanks to Jared Davis for suggesting these, and for providing seven
  small modifications to the community books to keep proofs from
  failing after the changes. (So, if you have a proof failure
  involving `plus' (+) that formerly succeeded, consider disabling
  one or more of these rules.) Here are the three new built-in
  theorems.

  Theorem: <commutativity-2-of-+>

    (defthm commutativity-2-of-+
            (equal (+ x (+ y z)) (+ y (+ x z))))

  Theorem: <fold-consts-in-+>

    (defthm fold-consts-in-+
            (implies (and (syntaxp (quotep x))
                          (syntaxp (quotep y)))
                     (equal (+ x (+ y z)) (+ (+ x y) z))))

  Theorem: <distributivity-of-minus-over-+>

    (defthm distributivity-of-minus-over-+
            (equal (- (+ x y)) (+ (- x) (- y))))

Quoting a comment in (defxdoc note-7-0 ...):

; Technical fix to encapsulate-fn: it now calls install-event with a namex of 0
; instead of nil in the case of an empty signature list.  As a result, (getprop
; nil 'absolute-event-number :none 'current-acl2-world (w state)) returns the
; true absolute event number for the introduction of the constant nil, rather
; than being increased every time we execute (encapsulate () ...).