## IN-ARITHMETIC-THEORY

designate ``current'' theory for some rewriting done in linear arithmetic
Major Section: EVENTS

Example:
(in-arithmetic-theory '(lemma1 lemma2))
General Form:
(in-arithmetic-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-arithmetic-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`

.
Warning: If `term`

involves macros such as `ENABLE`

and `DISABLE`

you will probably not get what you expect! Those macros are defined
relative to the `CURRENT-THEORY`

. But in this context you might
wish they were defined in terms of the ```CURRENT-ARITHMETIC-THEORY`

''
which is not actually a defined function. We do not anticipate that users
will repeatedly modify the arithmetic theory. We expect `term`

most often
to be a constant list of runes and so have not provided ``arithmetic theory
manipulation functions'' analogous to `CURRENT-THEORY`

and `ENABLE`

.

BECAUSE NO UNIQUE name is associated with an `in-arithmetic-theory`

event,
there is no way we can store the documentation string `doc-string`

in our il[documentation] data base. Hence, we actually prohibit `doc-string`

from having the form of an ACL2 documentation string;
see doc-string.

See non-linear-arithmetic.