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