In-theory
Designate ``current'' theory (enabling its rules)
Example:
(in-theory (set-difference-theories
(universal-theory :here)
'(flatten (:executable-counterpart flatten))))
General Form:
(in-theory term)
where term is a term that when evaluated will produce a theory (see
theories).
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.
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.
In-theory returns an error-triple. When the return is
without error, the value is of the form (mv nil
(:NUMBER-OF-ENABLED-RUNES k) state) where k is the length of the new
current theory. This value of k is what is printed when an
in-theory event evaluates without error at the top level.
