Major Section: THEORIES
Example: (intersection-theories (current-theory :here) (theory 'arith-patch)) General Form: (intersection-theories th1 th2)where
th2are theories (see theories). To each of the arguments there corresponds a runic theory. This function returns the intersection 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.