Updated :doc certify-book to reflect an imminent change to acl2-devel
regarding how the world is rolled back before the include-book phase
of certify-book.  Now, as suggested by Sol Swords, we no longer care
about make-event forms (in particular, with non-nil :check-expansion)
when determining the roll back.  Related to that is the following,
quoting :doc note-6-5:

  For calls of [make-event] made during the [include-book] phase of
  [certify-book], keyword :check-expansion no longer causes
  evaluation of the first argument of make-event; rather, the value
  of :check-expansion is simply used as the expansion. Thanks to Sol
  Swords for suggesting this change, which made it reasonable to
  ignore such make-event forms when determining the ``rolling back''
  before that include-book phase, as described in the next section.


git-svn-id: http://acl2-books.googlecode.com/svn/trunk@2550 303c5b2c-9740-0410-b014-fd8f9db7be32
Adding certify-book command to total-order.acl2, simply as a convenience for making the books in this directory by typing "make".  I understand that someone may decide to withdraw that support at some point, but in the meantime I find it handy, so I am making that .acl2 file like the others in this directory.

git-svn-id: http://acl2-books.googlecode.com/svn/trunk@2551 303c5b2c-9740-0410-b014-fd8f9db7be32