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.

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.