		Search-engine friendly clone of the ACL2 documentation.

Set-difference-theories

Difference of two theories

Example:
(set-difference-theories (current-theory :here)
                         '(fact (fact)))

General Form:
(set-difference-theories th1 th2)

where th1 and th2 are theories (see theories). To each of the arguments there corresponds a runic theory. This function returns the set-difference of those two runic theories, represented as a list and ordered chronologically. That is, a rune is in the result iff it is in the first runic theory but not in the second.

The standard way to ``disable'' a theory, lst, is: (in-theory (set-difference-theories (current-theory :here) lst)).

This ``function'' is actually a macro that expands to a term mentioning the single free variable world. When theory expressions are evaluated by in-theory or the :in-theory hint, world is bound to the current ACL2 world.