Major Section: EVENTS
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
in-theory. Specifically, the form
(defthmd NAME TERM ...)expands to:
(progn (defthmd NAME TERM ...) (with-output :off summary (in-theory (disable NAME))) (value-triple '(:defthmd NAME))).
defthmd commands are never redundant (see redundant-events).
Even if the
defthm event is redundant, then the
will still be executed.
The summary for the
in-theory event is suppressed. See defthm for