Theory Loading and Saving Commands

load

``load file-name'' causes the theory stored in file-name.wthy to be loaded into the workspace. If a theory has already been loaded, it is backed up on the desktop. Load sets the ``current theory'' environment variable to ``file-name'' as well. (walk command ``G'').

safesave

The safesave command has no arguments. It calls the ``storeall'' command with argument the ``current theory''. The ``walk'' interface version is ``S''.

storeall

``storeall file-name'' stores the current theory to file-name.wthy. It also sets the ``current theory'' environment variable to file-name. (walk command ``F'').

clear

The clear command erases the current theory and loads preambles (axioms always used). It does not affect other theories on the desktop. It sets the ``current theory'' to ``scratch'' (walk command ``C'').

clearpredicative

As ``clear'', and imposes predicativity restrictions on abstraction. Of technical interest only.

versiondate

This command (no parameter) displays the date of the version of the software being used.

script

``script file-name'' has the effect of the ML command ``use file-name.mk2''; files with the extension .mk2 are to be recognizable as proof scripts. script now uses a file parser independent of ML, also exploited by the noml alternative interface command.

The next two commands control prover output in ways that are sometimes convenient when running proof scripts.

setpause, setnopause:

setpause causes the prover to pause whenever it issues an error message. This is useful when running proof scripts. setnopause reverses this effect.

bequiet, speakup:

bequiet suppresses all output usually seen from proof scripts, except error messages. speakup reverses this effect, which is necessary if normal prover function is to be restored.