Major Section: THEORIES
Example: (disable fact (fact) associativity-of-app) General Form: (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.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).
