DEFTHMD

prove and name a theorem and then disable it 
Major Section:  EVENTS

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: 
(progn
  (defthmd NAME TERM ...)
  (with-output
   :off summary
   (in-theory (disable NAME)))
  (value NAME)).

Note that defthmd commands are never redundant (see redundant-events). Even if the defthm event is redundant, then the in-theory event will still be executed.

The summary for the in-theory event is suppressed. See defthm for documentation of defthm.