IN-THEORY

designate ``current'' theory (enabling its rules)
Major Section:  EVENTS

Example:
(in-theory (set-difference-theories
             (universal-theory :here)
             '(flatten (:executable-counterpart flatten))))

General Form:
(in-theory term :doc doc-string)
where term is a term that when evaluated will produce a theory (see theories), and doc-string is an optional documentation string not beginning with ``:doc-section ...''. Except for the variable world, term must contain no free variables. Term is evaluated with the variable world bound 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 doc-string from having the form of an ACL2 documentation string; see doc-string.

Note that it is often useful to surround in-theory events with local, that is, to use (local (in-theory ...)). This use of local in encapsulate events and books will prevent the effect of this theory change from being exported outside the context of that encapsulate or book.

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.