Major Section: THEORIES
Example: (union-theories (current-theory 'lemma3) (theory 'arith-patch))where
General Form: (union-theories th1 th2)
th2are theories (see theories). To each of the arguments there corresponds a runic theory. This function returns the union of those two runic theories, represented as a list and ordered chronologically.
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.