Uses of Class
fmrisc.Proving.Proof

Packages that use Proof

fmrisc.Communication
fmrisc.ProofNavigator
fmrisc.ProofNavigator.SWT
fmrisc.Proving
fmrisc.Semantics

Uses of Proof in fmrisc.Communication

Methods in fmrisc.Communication that return Proof

Proof

Store.readProof(FormulaSymbol symbol) Read proof for formula from store.

Methods in fmrisc.Communication with parameters of type Proof

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

Methods in fmrisc.ProofNavigator that return Proof

static Proof

State.getProof() get current proof

Methods in fmrisc.ProofNavigator with parameters of type Proof

static void	Main.setProof(Proof proof) Signal current proof.
static void	State.setProof(Proof proof) set current proof

Uses of Proof in fmrisc.ProofNavigator.SWT

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

void	ProofTree.setProof(Proof proof) Change tree to visualize denoted proof.
void	Top.setProof(Proof proof) Set the current proof.
static void	MainSWT.setProof(Proof proof) Set current proof.

Uses of Proof in fmrisc.Proving

Methods in fmrisc.Proving that return Proof

Proof	ProofState.getProof() get proof to which proof state belong
static Proof	Proof.newProof(FormulaSymbol symbol, boolean autoSimplify) 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.Proving with parameters of type Proof

ProofState(Proof proof)
Construct a skeleton proof state (all fields but the proof remain uninitialized).

ProofState(Proof proof, Environment env, Expression goal, boolean autoSimplify)
construct a root state from a single goal and without assumptions

Uses of Proof in fmrisc.Semantics

Methods in fmrisc.Semantics that return Proof

Proof

FormulaSymbol.getProof() Return proof of symbol.

Methods in fmrisc.Semantics with parameters of type Proof

void	FormulaSymbol.setProof(Proof proof) Set proof of symbol.