define a `static' theory (to enable or disable a set of rules)
Major Section:  EVENTS  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-static differs from
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 (in-theory (theory 'my-theory)).
Then the rule car-cons will be disabled, because it was disabled
at the time the expression (current-theory :here) was evaluated
when processing the deftheory of my-theory while including the
book. However, if we execute (in