world. When theory expressions
are evaluated by in-theory or the :in-theory hint, world is bound to
the current ACL2 world.
Major Section: THEORIES
Example:
(union-theories (current-theory 'lemma3)
(theory 'arith-patch))
General Form:
(union-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 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 :in-theory hint, world is bound to
the current ACL2 world.