Designate theory for some rewriting done for non-linear arithmetic

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)

where `world`, `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 `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-theory` and `enable`.