fmrisc.ProofNavigator.Commands

Class Lemma

java.lang.Object

fmrisc.ProofNavigator.Commands.CommandBase

fmrisc.ProofNavigator.Commands.ProofCommandBase

fmrisc.ProofNavigator.Commands.Lemma

All Implemented Interfaces:

Command, ProofCommand

public final class Lemma
extends ProofCommandBase

The "lemma" command: import other formulas.

Field Summary

Fields

Modifier and Type	Field and Description
static java.lang.String	Name

Constructor Summary

Constructors

Constructor and Description
Lemma(Identifier[] idents) Create a "lemma" command.

Method Summary

Modifier and Type	Method and Description
FormulaSymbol[]	getSymbols(Environment env) Return symbols of formulas referenced in lemma.
static Command	newCommand(org.w3c.dom.Node node) Convert DOM node to command.
void	printCore(java.io.PrintWriter out) Prints text representation on out (without new line termination).

Methods inherited from class fmrisc.ProofNavigator.Commands.ProofCommandBase

process, process

Methods inherited from class fmrisc.ProofNavigator.Commands.CommandBase

getName, toCommand, toNode, toString

Methods inherited from class java.lang.Object

equals, getClass, hashCode, notify, notifyAll, wait, wait, wait

Methods inherited from interface fmrisc.ProofNavigator.Commands.Command

toNode

Field Detail

Name

public static final java.lang.String Name

See Also:

Constant Field Values

Constructor Detail

Lemma

public Lemma(Identifier[] idents)

Create a "lemma" command.

Parameters:

idents - the identifiers of the formulas to be imported.

Method Detail

getSymbols

public FormulaSymbol[] getSymbols(Environment env)

Return symbols of formulas referenced in lemma.

Parameters:

env - the environment in which the symbols are looked up.

Returns:

the sequence of formula symbols.

newCommand

public static Command newCommand(org.w3c.dom.Node node)

Convert DOM node to command.

Parameters:

node - the DOM representation of the command.

Returns:

the command (null, if an error occured).

printCore

public void printCore(java.io.PrintWriter out)

Prints text representation on out (without new line termination).

Specified by:

printCore in class CommandBase

Parameters:

out - the stream on which the text is written