Package | Description |
---|---|
de.uka.ilkd.key.macros.scripts |
Proof script commands are a simple proof automation facility.
|
Modifier and Type | Class and Description |
---|---|
class |
AssertCommand
Halts the script if some condition is not met.
|
class |
AssumeCommand
The assume command takes one argument: * a formula to which the command is
applied
|
class |
AutoCommand
The AutoCommand invokes the automatic strategy "Auto".
|
class |
AxiomCommand
The axiom command takes one argument: a formula to which the command is
applied.
|
class |
CutCommand
The command object CutCommand has as scriptcommand name "cut"
As parameters:
a formula with the id "#2"
|
class |
EchoCommand
A simple "echo" command for giving feedback to human observers during lengthy
executions.
|
class |
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.
|
class |
InstantiateCommand
instantiate var=a occ=2 with="a_8" hide
|
class |
JavascriptCommand |
class |
LetCommand |
class |
MacroCommand |
class |
RewriteCommand
This class provides the command
rewrite . |
class |
RuleCommand
Command that applies a calculus rule All parameters are passed as strings and
converted by the command.
|
class |
SaveInstCommand
Special "Let" usually to be applied immediately after a manual rule
application.
|
class |
SaveNewNameCommand
Special "Let" usually to be applied immediately after a manual rule
application.
|
class |
SchemaVarCommand |
class |
ScriptCommand |
class |
SelectCommand |
class |
SetCommand |
class |
SetEchoCommand
A simple "echo" command for giving feedback to human observers during lengthy
executions.
|
class |
SetFailOnClosedCommand
Sets the behavior if an already closed proof is encountered: Either throw an
exception (default behavior, sensible for specially tailored scripts for
which a prematurely closed proof is unexpected) or peacefully terminate (if
the script addresses different problems of different complexity in a
try-and-error manner, etc.).
|
class |
SMTCommand |
class |
TryCloseCommand
The script command tryclose" has two optional arguments:
steps: INTEGER number of steps to use
#2: STRING the number of the branch which should be closed
If #2 is not given or not a number, the TryClose macro is applied to all open
goals.
|
Copyright © 2003-2019 The KeY-Project.