Define a `static' theory (to enable or disable a set of rules)

This macro provides a variant of `deftheory`, such that the
resulting theory is the same at `include-book` time as it was at `certify-book` time.

We assume that the reader is familiar with theories; see deftheory. We begin here by illustrating how `deftheory`. Suppose for example that the following events are the
first two events in a book, where that book is certified in the initial ACL2
world (see ground-zero).

(deftheory my-theory (current-theory :here)) (deftheory-static my-static-theory (current-theory :here))

Now suppose we include that book after executing the following event.

(in-theory (disable car-cons))

Suppose that later we execute

General Form: (deftheory-static name term)

The arguments are handled the same as for `deftheory`. Thus,
`world`, `world` bound to the current world (see
world) and the resulting theory is then converted to a *runic
theory* (see theories) and associated with

As for `deftheory`, the value returned is the length of the resulting
theory.

We conclude with an optional discussion about the implementation of
`make-event`. The
following macroexpansion of the

ACL2 !>:trans1 (deftheory-static my-static-theory (current-theory :here)) (MAKE-EVENT (LET ((WORLD (W STATE))) (LIST 'DEFTHEORY 'MY-STATIC-THEORY (LIST 'QUOTE (CURRENT-THEORY :HERE))))) ACL2 !>

The idea is that upon evaluation of this `let` expression to obtain a form