DISABLE

deletes names from current theory 
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: 

(in-theory (disable name1 name2 ... namek)) ; globally
:in-theory (disable name1 name2 ... namek)  ; locally
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).