		Search-engine friendly clone of the ACL2 documentation.

Defund2-implementation

Implementation of defund2.

Macro: defund2

(defmacro defund2 (sofun &rest rest)
  (list 'progn
        (list* 'defund sofun rest)
        (list 'defsoft sofun)))

Macro: defund2

(defmacro acl2::defund2 (&rest args)
  (list* 'defund2 args))