Major Section: EVENTS
Example: (in-theory (set-difference-theories (universal-theory :here) '(flatten (:executable-counterpart flatten))))where
General Form: (in-theory term :doc doc-string)
termis a term that when evaluated will produce a theory (see theories), and
doc-stringis an optional documentation string not beginning with ``
:doc-section...''. Except for the variable
termmust contain no free variables.
Termis evaluated with the variable
worldbound to the current world to obtain a theory and the corresponding runic theory (see theories) is then made the current theory. Thus, immediately after the
in-theory, a rule is enabled iff its rule name is a member of the runic interpretation (see theories) of some member of the value of
term. See theory-functions for a list of the commonly used theory manipulation functions.
Because no unique name is associated with an
in-theory event, there
is no way we can store the documentation string
doc-string in our
documentation data base. Hence, we actually prohibit
from having the form of an ACL2 documentation string;
Also see hints for a discussion of the
:in-theory hint, including some
explanation of the important point that an
:in-theory hint will always be
evaluated relative to the current ACL2 logical world, not relative to
the theory of a previous goal.