## IN-ARITHMETIC-THEORY

designate theory for some rewriting done for non-linear arithmetic
Major Section: EVENTS

We assume familiarity with theories; in particular, see in-theory for
the normal way to set the current theory. Here, we discuss an analogous
event that pertains only to non-linear arithmetic
(see non-linear-arithmetic).

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 used by non-linear arithmetic
(see non-linear-arithmetic).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] database. Hence, we actually prohibit `doc-string`

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

See non-linear-arithmetic.