Quoting :doc note-6-5:

  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.


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