union two theories
Major Section:  THEORIES

(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.