Next: Environment Starting and other
Up: Appendix: Reference for Individual
- ``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'').
- The safesave command has no arguments. It calls the
``storeall'' command with argument the ``current theory''. The
``walk'' interface version is ``S''.
- ``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'').
- 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
- As ``clear'', and imposes predicativity
restrictions on abstraction. Of technical interest only.
- This command (no parameter) displays the date of
the version of the software being used.
- ``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
- 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.
Fri Sep 5 16:28:58 MDT 1997