Implementation of defun2.
Macro: defun2
(defmacro defun2 (sofun &rest rest) (list 'progn (list* 'defun sofun rest) (list 'defsoft sofun)))
(defmacro acl2::defun2 (&rest args) (list* 'defun2 args))
