Simplify-defun-sk-programmatic
Programmatic interface to simplify-defun-sk
Call simplify-defun-sk-programmatic exactly as you would call
simplify-defun-sk, except that arguments are not automatically quoted;
so avoid using arguments of the form (:eval x). Unlike
simplify-defun-sk, simplify-defun-sk-programmatic does not introduce
a new definition or theorem. Rather, it returns the encapsulate form
that would be evaluated by simplify-defun-sk — that is, the form
displayed by a corresponding call of show-simplify-defun-sk.
