|
Class Summary |
| Assume |
Commnand "assume": split proof state by an assumption and its proof. |
| Auto |
Command "auto": try to close state by automatic instantiation
of quantified formulas. |
| AutoStar |
command "autostar": apply auto to current node and its successor siblings. |
| Case |
The "case" command: split state into multiple cases. |
| CommandBase |
Base class of commands. |
| ContextC |
Command "newcontext": change context to denoted path. |
| CounterExample |
Command "counterexample": show potential counterexample for current
state (may be time-consuming) |
| DeclarationC |
Virtual command "declaration": process declaration in current environment |
| Decompose |
command "decompose": decompose proof state by repeated skolemization
and flattening. |
| Empty |
The virtual "empty" command: do nothing. |
| EnvironmentC |
Command "environment": show environment (global or of current state). |
| Expand |
Command "expand": expand a definition. |
| Flatten |
Command "flatten": decompose compound formulas without splitting the state. |
| Flip |
|
| FormulaC |
Command "formula": print value of formula identifier. |
| Goal |
|
| Goto |
The "goto" command: goto an open proof state. |
| Induction |
Command "induction": induction on a univerally quantified NAT/INT variable. |
| Instantiate |
The "instantiate" command: instantiate a quantified formula. |
| Lemma |
The "lemma" command: import other formulas. |
| Next |
The "next" command: goto next open proof state. |
| Open |
The "open" command: display the list of open states. |
| Option |
The "option" command: set a system option. |
| Prev |
The "prev" command: goto previous open proof state. |
| ProofC |
Command "proof": print proof tree. |
| ProofCommandBase |
Base class of proof commands. |
| Prove |
"prove": prove goal formula. |
| Proved |
|
| Quit |
"quit": quit from current proof or session. |
| Read |
Command "read": read command from denoted file. |
| Redo |
The "redo" command: goto an open proof state and redo its proof. |
| Scatter |
command "scatter": scatter proof state by repeated decomposition
and goalsplitting. |
| Simplify |
Command "simplify": simplify a proof state. |
| Skolemize |
|
| Split |
Command "split": split a proof state. |
| StateC |
Command "state": print denoted state. |
| TCC |
"tcc": print type checking conditions generated from last declaration. |
| TypeAxiom |
The "typeaxiom" command: instantiate a quantified type axiom. |
| TypeC |
Command "type": print value of type identifier. |
| Undo |
The "undo" command: goto a closed proof state and undo its proof. |
| ValueC |
Command "value": print value of value identifier. |