Major Section: EVENTS
Examples: (remove-untouchable my-var nil) (remove-untouchable set-mem t)General Form: (remove-untouchable name{s} fn-p :doc doc-string)
where name{s} is a non-nil symbol or a non-nil true list of symbols,
fn-p is any value (but generally nil or t), and doc-string
is an optional documentation string not beginning with
``:doc-section ...''. If name{s} is a symbol it is treated as the
singleton list containing that symbol. The effect of this event is to remove
the given symbols from the list of ``untouchable variables'' in the current
world if fn-p is nil, else to remove the symbols into the list of
``untouchable functions''. This event is redundant if no symbol listed is a
member of the appropriate untouchables list (variables or functions).
Note that remove-untouchable is illegal by default, since it can be used
to provide access to ACL2 internal functions and data structures that are
intentionally made untouchable for the user. If you want to call it, you
must first create an active trust tag; see defttag.
Also See push-untouchable.