The following from :doc note-6-5 is not new, except for the last part
thanking Jared, which pertains to a fix made in this check-in.

  One of the steps performed by [certify-book] has traditionally been
  to check for local incompatibilities (see [local-incompatibility])
  after admitting all the events in the book. This step involved
  rolling back the logical [world] to what it was at the start of
  certification, and then including the book (see [include-book]). As
  an optimization, we now avoid rolling back the world more than
  necessary; see [certify-book], specifically the discussion of Step
  3. Thanks to Sol Swords for requesting this optimization, and also
  to Jared Davis for alerting us to an issue that turned out to be
  caused by a bug in our initial implementation.


git-svn-id: http://acl2-devel.googlecode.com/svn/trunk@1240 5d84a466-a78b-0930-a311-59b22171a541
Quoting :doc note-6-5:

  (ACL2(h) only) We fixed a soundness bug involving the interaction of
  [stobj-let] and [memoize], which thus is only a bug in ACL2(h) (see
  [hons-and-memoization]), not in ACL2. The fix was to add code to
  stobj-let that clears the memoization table for the parent stobj if
  any child stobj is updated.


git-svn-id: http://acl2-devel.googlecode.com/svn/trunk@1242 5d84a466-a78b-0930-a311-59b22171a541
Fixed ignore declaration for ACL2 (was OK already for ACL2(h)).

git-svn-id: http://acl2-devel.googlecode.com/svn/trunk@1243 5d84a466-a78b-0930-a311-59b22171a541