Major Section: PROOF-CHECKER
Example: (unsave assoc-of-append) General Form: (unsave name)
name
Also see acl2-pc::save and see retrieve.