Defthmd
Prove and name a theorem and then disable it
Use defthmd instead of defthm when you want to disable
a theorem immediately after proving it. This macro has been provided for
users who prefer working in a mode where theorems are only enabled when
explicitly directed by :in-theory. Specifically, the form
(defthmd NAME TERM ...)
expands to the following, except that some output is inhibited for the
in-theory and value-triple events:
(progn
(defthm NAME TERM ...)
(in-theory (disable NAME))
(value-triple '(:defthmd NAME))).
Defthmd events are generally not redundant, because the generated
in-theory event is not redundant. This default can be changed; see
set-in-theory-redundant-okp.
See defthm for documentation of defthm.
