fmrisc.ProofNavigator.Commands
Interface ProofCommand

All Superinterfaces:
Command
All Known Implementing Classes:
Assume, Auto, AutoStar, Case, CounterExample, Decompose, Expand, Flatten, Flip, Goal, Goto, Induction, Instantiate, Lemma, Next, Open, Option, Prev, ProofCommandBase, Proved, Redo, Scatter, Simplify, Skolemize, Split, TypeAxiom, Undo

public interface ProofCommand
extends Command

Interface to proof commands.


Method Summary
 ProofState[] process(ProofState state)
          process proof state.
 
Methods inherited from interface fmrisc.ProofNavigator.Commands.Command
process, toNode
 

Method Detail

process

ProofState[] process(ProofState state)
process proof state.

Parameters:
state - the state to which the proof command is applied (remains unchanged)
Returns:
a sequence of children of state generated by the command (null, if the command did not generate any)