E/D

enable/disable rules 
Major Section:  THEORIES

The macro e/d creates theory expressions for use in in-theory hints and events. It provides a convenient way to enable and disable simultaneously, without having to write arcane theory expressions. 

Examples:
(e/d (lemma1 lemma2))          ; equivalent to (enable lemma1 lemma2)
(e/d () (lemma))               ; equivalent to (disable lemma)
(e/d (lemma1) (lemma2 lemma3)) ; Enable lemma1 then disable lemma2, lemma3.
(e/d () (theory1) (theory2))   ; Disable theory1 then enable theory2.


General Form:
(e/d enables-0 disables-0 ... enables-n disables-n)
where each enables-i and disables-i is a list of runic designators; see theories, see enable, and see disable.

The e/d macro takes any number of lists suitable for the enable and disable macros, and creates a theory that is equal to (current-theory :here) after executing the following commands.

(in-theory (enable . enables-0)) (in-theory (disable . disables-0)) ... (in-theory (enable . enables-n)) (in-theory (disable . disables-n))