| | | B.1.2 newcontext: Start New Declaration Context |
newcontext
newcontext "path"
In declaration mode.
The command creates a new and empty declaration
environment erasing from the system memory all previous constant
declarations. The command associates this environment to a directory in the
file system (creating the directory, if it does not yet exist) for
persistently storing representations of the constants declared in the new
environment and of proofs of formulas performed. If newcommand is
invoked without argument, this directory is named ProofNavigator
and is located in the current working directory of the system (unless the
system has been started with the option --context, see
Appendix Invocation). If the
command is invoked with an argument "path", the directory with the
name and location denoted by path is (if necessary created and)
used rather than the default directory.
| | | B.1.2 newcontext: Start New Declaration Context |