ACL2-PC::IN-THEORY
(primitive)
set the current proof-checker theory
Major Section: PROOF-CHECKER-COMMANDS
Example:
(in-theory
(union-theories *s-prop-theory* '(true-listp binary-append)))
General Form:
(in-theory &optional atom-or-theory-expression)
If the argument is not supplied, then this command sets the
current proof-checker theory (see below for explanation) to agree
with the current ACL2 theory. Otherwise, the argument should be a
theory expression, and in that case the proof-checker theory is set
to the value of that theory expression.
The current proof-checker theory is used in all calls to the ACL2
theorem prover and rewriter from inside the proof-checker. Thus,
the most recent in-theory instruction in the current state-stack has
an effect in the proof-checker totally analogous to the effect
caused by an in-theory hint or event in ACL2. However, in-theory
instructions in the proof-checker have no effect outside the
proof-checker's interactive loop.
If the most recent in-theory instruction in the current state of the
proof-checker has no arguments, or if there is no in-theory
instruction in the current state of the proof-checker, then the
proof-checker will use the current ACL2 theory. This is true even
if the user has interrupted the interactive loop by exiting and
changing the global ACL2 theory. However, if the most recent
in-theory instruction in the current state of the proof-checker had
an argument, then global changes to the current theory will have no
effect on the proof-checker state.
