Defun-sk2-implementation
Implementation of defun-sk2.
Macro: defun-sk2
(defmacro defun-sk2 (sofun &rest rest)
(list 'progn
(list* 'defun-sk sofun rest)
(list 'defsoft sofun))) Macro: defun-sk2
(defmacro acl2::defun-sk2 (&rest args)
(list* 'defun-sk2 args))
