Major Section: THEORIES
Example: (theory 'my-theory)where
General Form: (theory name)
nameis the name of a previously executed
deftheoryevent. Returns the named theory. See theories.
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.