Fixed a documentation bug: namely, in the criterion for redundancy of
encapsulate events in :doc encapsulate.

Slightly extended :doc redo-flat in collaboration with Sol Swords.

Clarified in the documentation for progn and encapsulate that when any
sub-event fails, the world is rolled back.  Thanks to Nathan Wetzler
for pointing out that this documentation was missing.

Quoting :doc note-6-5:

  The test for redundancy of [encapsulate] [events] has been made more
  efficient. Also, while the criterion itself remains unchanged, the
  documentation has been made more accurate; see
  [redundant-encapsulate]. We observed more than a 2% reduction in
  time for the ``everything'' regression target, but we observed more
  than 23% of the time eliminated for the form (time$ (include-book
  "doc/top" :dir :system)) after building the documentation. Thanks
  to David Rager for bringing that particular book to our attention,
  as one that took a long time to include.


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