Uses of Class
fmrisc.ProofNavigator.Proving.Proof

Packages that use Proof

Package	Description
fmrisc.ProgramExplorer
fmrisc.ProgramExplorer.Proving
fmrisc.ProofNavigator
fmrisc.ProofNavigator.Communication
fmrisc.ProofNavigator.Proving
fmrisc.ProofNavigator.Semantics
fmrisc.ProofNavigator.SWT

Uses of Proof in fmrisc.ProgramExplorer

Methods in fmrisc.ProgramExplorer with parameters of type Proof

Modifier and Type	Method and Description
static void	Main.proofDone(Proof proof) Called if a proof is completed by the ProofNavigator.

Uses of Proof in fmrisc.ProgramExplorer.Proving

Methods in fmrisc.ProgramExplorer.Proving that return Proof

Modifier and Type	Method and Description
Proof	ProofNavigatorProblem.getProof() Get current proof, possibly load it from file.

Methods in fmrisc.ProgramExplorer.Proving with parameters of type Proof

Modifier and Type	Method and Description
static void	ProofNavigatorProblem.proofDone(Proof proof) Called if a proof is completed by the ProofNavigator.

Uses of Proof in fmrisc.ProofNavigator

Methods in fmrisc.ProofNavigator that return Proof

Modifier and Type	Method and Description
static Proof	State.getProof() get current proof

Methods in fmrisc.ProofNavigator with parameters of type Proof

Modifier and Type	Method and Description
static void	Main.proofDone(Proof proof) Signal that proof is completed.
static void	State.setProof(Proof proof) set current proof
static void	Main.setProof(Proof proof) Signal current proof.

Uses of Proof in fmrisc.ProofNavigator.Communication

Methods in fmrisc.ProofNavigator.Communication that return Proof

Modifier and Type	Method and Description
Proof	Store.readProof(FormulaSymbol symbol) Read proof for formula from store.

Methods in fmrisc.ProofNavigator.Communication with parameters of type Proof

Modifier and Type	Method and Description
boolean	Store.write(Proof proof) Write proof to store updating the dependencies file.
java.io.File	Presenter.writeProofIndex(Proof proof) Write index of proof to file suitable for later display of proof states.

Uses of Proof in fmrisc.ProofNavigator.Proving

Methods in fmrisc.ProofNavigator.Proving that return Proof

Modifier and Type	Method and Description
Proof	ProofState.getProof() get proof to which proof state belong
static Proof	Proof.newProof(FormulaSymbol symbol, boolean autoSimplify, State.ProverVersion proverVersion, boolean firstOrder, boolean toLogical) Construct new proof for formula denoted by symbol.
static Proof	Proof.toProof(FormulaSymbol symbol, org.w3c.dom.Node node) Construct skeleton proof from DOM representation.

Constructors in fmrisc.ProofNavigator.Proving with parameters of type Proof

Constructor and Description
ProofState(Proof proof) Construct a skeleton proof state (all fields but the proof remain uninitialized).
ProofState(Proof proof, Environment env, Expression goal, boolean autoSimplify, State.ProverVersion proverVersion, boolean firstOrder, boolean toLogical) construct a root state from a single goal and without assumptions

Uses of Proof in fmrisc.ProofNavigator.Semantics

Methods in fmrisc.ProofNavigator.Semantics that return Proof

Modifier and Type	Method and Description
Proof	FormulaSymbol.getProof() Return proof of symbol.

Methods in fmrisc.ProofNavigator.Semantics with parameters of type Proof

Modifier and Type	Method and Description
void	FormulaSymbol.setProof(Proof proof) Set proof of symbol.

Uses of Proof in fmrisc.ProofNavigator.SWT

Methods in fmrisc.ProofNavigator.SWT with parameters of type Proof

Modifier and Type	Method and Description
void	ProofTree.setProof(Proof proof) Change tree to visualize denoted proof.
static void	MainSWT.setProof(Proof proof, boolean enabled) Set current proof.
void	Top.setProof(Proof proof, boolean enabled) Set the current proof.