|
|
|---|
|
|
|
|---|
Compound command for the interactive proof-builder
The interactive proof-builder supports the definition of compound commands, called ``macro commands'', which expand into zero or more other commands. Some of these are ``atomic'' macro commands; these are viewed as a single command step when completed successfully.
More documentation may be written on the interactive proof-builder. For now, we simply point out that there are lots of examples
of the use of
Also see toggle-pc-macro for how to change a macro command to an atomic macro command, and vice versa.