DEFUND

define a function symbol and then disable it 
Major Section:  EVENTS

Use defund instead of defun when you want to disable a function immediately after its definition. This macro has been provided for users who prefer working in a mode where functions are only enabled when explicitly directed by :in-theory. Specifically, the form 

(defund NAME FORMALS ...)
expands to: 
(progn
  (defun NAME FORMALS ...)
  (with-output
   :off summary
   (in-theory (disable NAME)))
  (value NAME)).
Only the :definition rule (and, for recursively defined functions, the :induction rule) for the function are disabled, and the summary for the in-theory event is suppressed.

Note that defund commands are never redundant (see redundant-events). If the function has already been defined, then the in-theory event will still be executed.

See defun for documentation of defun.