Theory handling commands:

clear:

This command takes a unit argument. It clears the current theory and resets the theory name to ``scratch''.

cleartheories:

This command takes a unit argument. It clears all theories and resets the theory name to ``scratch''.

backuptheory:

This command takes a unit argument. It saves the current theory to the desktop. Automatically invoked by several other commands.

gettheory:

This command takes a single string argument. It gets the theory named by its argument from the desktop. It backs up the current theory unless it is the same as the theorem named by the argument. With the new incremental backup scheme, you will see a sequence of theories loaded.

droptheory:

This command takes a single string argument. It deletes the theory named by its argument from the desktop.

storeall:

This command takes a single string argument. It stores the current theory in a stored theory file named by the argument (with extension .sav.wat). It also changes the theory name to match the argument.

safesave:

This command takes a unit argument. Just as storeall; the argument supplied to storeall is the current theory name.

load:

This command takes a single string argument. It loads the theory in the stored theory file named by the argument (with the extension .sav.wat) and changes the theory name. The previous theory and the new theory are backed up on the desktop. With the new incremental backup scheme, you may see a sequence of theories loaded. Also, it is now necessary to have .sav.wat files for all precursor theories of the theories being loaded.

script:

This command takes a single string argument. It runs the script file named by the argument (with extension .wat). It changes the theory name to match the argument and stores it to a file and to the desktop.

demo:

As script, except that the prover echoes command lines and pauses before and after each command entered by the user. In the newest version, the pauses take one to the ``secure shell''; one can issue ; to see the next line or e; to break out, or one can issue secure commands. (for old versions: in demo mode, one can type ``q'' to quit at most pauses, ``d'' to leave demo mode and finish execution of the script, and ``s'' to invoke the noml shell (after typing quit(); the script will resume, still in demo mode)).

demoremark:

This command takes a string argument; in a script in demo mode, the string will be displayed as a remark.

noml:

This command takes a unit argument. It invokes the no-ML interface; essentially, the standard input is hooked up to the script processor.

makescript:

This command takes a string argument. It clears the current autoscript file and calls noml, creating a new script file when noml is exited. The script file is named by the argument with the extension .log.wat. Automatically generated script files contain displays of theorems proved in comments following their proofs. The contents of script and load commands are not replicated in automatically generated scripts. This command cannot be nested.

truescript:

In the noml interface, this command should be used in place of script. script should be used in scripts, no matter what the interface. This is obsolete.

reset:

This command takes a unit argument. Run this command when you have broken out of a script using Control-C. Not available in the noml interface.