Uses of Interface
fmrisc.ProofNavigator.Commands.ProofCommand

Packages that use ProofCommand

Package	Description
fmrisc.ProofNavigator.Commands

Uses of ProofCommand in fmrisc.ProofNavigator.Commands

Classes in fmrisc.ProofNavigator.Commands that implement ProofCommand

Modifier and Type	Class and Description
class	Assume Commnand "assume": split proof state by an assumption and its proof.
class	Auto Command "auto": try to close state by automatic instantiation of quantified formulas.
class	AutoStar command "autostar": apply auto to current node and its successor siblings.
class	Case The "case" command: split state into multiple cases.
class	CounterExample Command "counterexample": show potential counterexample for current state (may be time-consuming)
class	Decompose command "decompose": decompose proof state by repeated skolemization and flattening.
class	Expand Command "expand": expand a definition.
class	Flatten Command "flatten": decompose compound formulas without splitting the state.
class	Flip Command "flip": flip a formula from goal position to assumption position or vice versa.
class	Goal Command "goal": let a formula become the single goal.
class	Goto The "goto" command: goto an open proof state.
class	Induction Command "induction": induction on a univerally quantified NAT/INT variable.
class	Instantiate The "instantiate" command: instantiate a quantified formula.
class	Lemma The "lemma" command: import other formulas.
class	Next The "next" command: goto next open proof state.
class	Open The "open" command: display the list of open states.
class	Option The "option" command: set a system option.
class	Prev The "prev" command: goto previous open proof state.
class	ProofCommandBase Base class of proof commands.
class	Proved Pseudo-command "proved": indicate the termination of a proof branch.
class	Redo The "redo" command: goto an open proof state and redo its proof.
class	Scatter command "scatter": scatter proof state by repeated decomposition and goalsplitting.
class	Simplify Command "simplify": simplify a proof state.
class	Skolemize Command "skolemize": skolemize universal formulas in goal position and existential formulas in assumption position.
class	Split Command "split": split a proof state.
class	TypeAxiom The "typeaxiom" command: instantiate a quantified type axiom.
class	Undo The "undo" command: goto a closed proof state and undo its proof.