Major Section: PROOF-CHECKER
Example: (toggle-pc-macro pro)Change
profrom an atomic macro command to an ordinary one (or vice-versa, if
prohappens 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-tpis supplied and not
nil, then it should be the new type (the symbol
atomic-macro, in any package), or else there is no change.