Deletes names from current theory
(disable fact (:e fact) associativity-of-app)
(disable name1 name2 ... namek)
where each namei is a runic designator; see theories. The
result is the theory that contains all the names in the current theory except
those listed. Note that this is merely a function that returns a theory. The
result is generally a very long list of runes and you will probably
regret printing it.
For related utilities, see enable and see e/d.
The standard way to ``disable'' a fixed set of names, is as follows; see
hints and see in-theory.
:in-theory (disable name1 name2 ... namek) ; in a hint
(in-theory (disable name1 name2 ... namek)) ; as an event
(local ; often desirable, to avoid exporting from the current context
(in-theory (disable name1 name2 ... namek)))
Note that all the names are implicitly quoted. If you wish to disable a
computed list of names, lst, use the theory expression
(set-difference-theories (current-theory :here) lst).