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