TOGGLE-PC-MACRO
change an ordinary macro command to an atomic macro, or vice-versa
Major Section: PROOF-CHECKER
Example:
(toggle-pc-macro pro)
Change pro from an atomic macro command to an ordinary one (or
vice-versa, if pro happens to be an ordinary macro command)
General Form:
(toggle-pc-macro name &optional new-tp)
If name is an
atomic macro command then this turns it into an ordinary one, and
vice-versa. However, if new-tp is supplied and not nil, then it
should be the new type (the symbol macro or atomic-macro, in any
package), or else there is no change.
