Uses of Class
fmrisc.Semantics.FormulaSymbol

Packages that use FormulaSymbol

fmrisc.Communication
fmrisc.ProofNavigator.Commands
fmrisc.Proving
fmrisc.Semantics
fmrisc.Syntax

Uses of FormulaSymbol in fmrisc.Communication

Methods in fmrisc.Communication with parameters of type FormulaSymbol

boolean	Store.existsProof(FormulaSymbol symbol) Check whether store holds proof of formula.
Proof	Store.readProof(FormulaSymbol symbol) Read proof for formula from store.

Uses of FormulaSymbol in fmrisc.ProofNavigator.Commands

Methods in fmrisc.ProofNavigator.Commands that return FormulaSymbol

FormulaSymbol[]

Lemma.getSymbols(Environment env) Return symbols of formulas referenced in lemma.

Uses of FormulaSymbol in fmrisc.Proving

Methods in fmrisc.Proving that return FormulaSymbol

FormulaSymbol

Proof.getSymbol() get symbol of formula proved

Methods in fmrisc.Proving with parameters of type FormulaSymbol

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.

Uses of FormulaSymbol in fmrisc.Semantics

Methods in fmrisc.Semantics that return FormulaSymbol

FormulaSymbol	Environment.getFormulaSymbol(Identifier name) returns symbol associated to name (null, if none)
FormulaSymbol	FormulaTable.getSymbol(Identifier name) returns symbol associated to name (null, if none)
FormulaSymbol	FormulaTable.put(FormulaDeclIdentifier key, Expression formula, boolean axiom, Environment env) put formula in formula table
FormulaSymbol	Environment.putFormula(FormulaDeclIdentifier name, Expression formula, boolean axiom) put formula in environment
FormulaSymbol	Environment.putFormulaDeclaration(FormulaDeclaration fdecl) put formula declaration into environment

Uses of FormulaSymbol in fmrisc.Syntax

Methods in fmrisc.Syntax that return FormulaSymbol

FormulaSymbol

FormulaDeclIdentifier.getSymbol() returns formula symbol