See: Description
| Interface | Description |
|---|---|
| ProofScriptCommand<T> |
A
ProofScriptCommand is an executable mutation on the given proof. |
| Class | Description |
|---|---|
| AbstractCommand<T> |
Inheritance:
|
| ActivateCommand |
Command for re-activating the first open (not necessarily enabled)
Goal after a "leave" command. |
| AssumeCommand |
The assume command takes one argument: * a formula to which the command is
applied
|
| AssumeCommand.FormulaParameter | |
| AutoCommand |
The AutoCommand invokes the automatic strategy "Auto".
|
| AutoCommand.Parameters | |
| CutCommand |
The command object CutCommand has as scriptcommand name "cut"
As parameters:
a formula with the id "#2"
|
| CutCommand.Parameters | |
| EchoCommand |
A simple "echo" command for giving feedback to human observers during lengthy
executions.
|
| EchoCommand.Parameters | |
| EngineState | |
| ExitCommand | |
| FocusOnSelectionAndHideCommand |
Hide all formulas that are not selected
Parameter:
* The sequent with those formulas that should not be hidden
Created by sarah on 1/12/17.
|
| FocusOnSelectionAndHideCommand.Parameters | |
| InstantiateCommand |
instantiate var=a occ=2 with="a_8" hide
instantiate formula="\forall int a; phi(a)" with="a_8"
|
| InstantiateCommand.Parameters | |
| InstantiateCommand.TacletNameFilter | |
| JavascriptCommand | |
| JavascriptCommand.JavascriptInterface | |
| JavascriptCommand.Parameters | |
| LeaveCommand | |
| LetCommand | |
| MacroCommand | |
| MacroCommand.Parameters | |
| NoArgumentCommand | |
| ProofScriptEngine | |
| RewriteCommand |
This class provides the command
rewrite. |
| RewriteCommand.Parameters |
Parameters for the
RewriteCommand |
| RuleCommand |
Command that applies a calculus rule All parameters are passed as strings and
converted by the command.
|
| RuleCommand.Parameters | |
| RuleCommand.TacletNameFilter | |
| SaveInstCommand |
Special "Let" usually to be applied immediately after a manual rule
application.
|
| SaveNewNameCommand |
Special "Let" usually to be applied immediately after a manual rule
application.
|
| SaveNewNameCommand.Parameters | |
| SchemaVarCommand | |
| SchemaVarCommand.Parameters | |
| ScriptCommand | |
| ScriptCommand.Parameters | |
| ScriptLineParser | |
| ScriptNode | |
| ScriptTreeParser | |
| SelectCommand | |
| SetCommand | |
| SetCommand.Parameters | |
| SetEchoCommand |
A simple "echo" command for giving feedback to human observers during lengthy
executions.
|
| SetEchoCommand.Parameters | |
| SettingsCommand |
This command is used to set variables in the proof environment.
|
| SettingsCommand.Parameters | |
| SkipCommand | |
| SMTCommand | |
| SMTCommand.SMTCommandArguments | |
| TryCloseCommand |
The script command tryclose" has two optional arguments:
steps: INTEGER number of steps to use
#2: STRING the branch which should be closed
TryClose tries to close the specified branch.
|
| TryCloseCommand.TryCloseArguments |
| Enum | Description |
|---|---|
| ScriptLineParser.State |
The state of the regular expression parser.
|
| Exception | Description |
|---|---|
| ScriptException |
ProofScriptCommand,
ProofScriptEngine,
EngineState