Major Section: THEORIES
Example: (set-difference-theories (current-theory :here) '(fact (fact)))where
General Form: (set-difference-theories th1 th2)
th2are 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,
(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
world is bound to
the current ACL2 world.