Defthy
Define a theory (to enable or disable a set of rules)
See deftheory. The defthy macro is simply a convenient
macro for deftheory that supports a limited notion of redundancy; see
redundant-events. Specifically: a call (defthy name expr) expands
to the corresponding event (deftheory name expr :redundant-okp t).
