Quoting :doc note-6-4:

| It had been possible to update a stobj (either an ordinary stobj or an
| abstract stobjs) so that it no longer satisfies its recognizer predicate.
| This soundness bug has been fixed.  Thanks to Jared Davis and Sol Swords for
| pointing out this bug, making useful observations about the issue, and
| sending proofs of nil, one of which may be found in a Lisp comment in the
| ACL2 sources at (deflabel note-6-4 ...).


git-svn-id: http://acl2-devel.googlecode.com/svn/trunk@1127 5d84a466-a78b-0930-a311-59b22171a541
Updated CS dept. zip code.

git-svn-id: http://acl2-devel.googlecode.com/svn/trunk@1129 5d84a466-a78b-0930-a311-59b22171a541
Made minor improvements to :doc NESTED-STOBJS.

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