Class and Description |
---|
Sequent
This class represents a sequent.
|
SequentFormula
A sequent formula is a wrapper around a formula that occurs
as top level formula in a sequent.
|
Term
In contrast to the distinction of formulas and terms as made by most of the
inductive definitions of the syntax of a logic, an instance of this class can
stand for a term or a formula.
|
Class and Description |
---|
Named
This interface has to be implemented by all logic signature elements, which
are identified by their name.
|
Term
In contrast to the distinction of formulas and terms as made by most of the
inductive definitions of the syntax of a logic, an instance of this class can
stand for a term or a formula.
|
Class and Description |
---|
Name
A Name object is created to represent the name of an object which usually
implements the interface
Named . |
Named
This interface has to be implemented by all logic signature elements, which
are identified by their name.
|
Term
In contrast to the distinction of formulas and terms as made by most of the
inductive definitions of the syntax of a logic, an instance of this class can
stand for a term or a formula.
|
Class and Description |
---|
Name
A Name object is created to represent the name of an object which usually
implements the interface
Named . |
Named
This interface has to be implemented by all logic signature elements, which
are identified by their name.
|
NamespaceSet |
Term
In contrast to the distinction of formulas and terms as made by most of the
inductive definitions of the syntax of a logic, an instance of this class can
stand for a term or a formula.
|
Class and Description |
---|
Name
A Name object is created to represent the name of an object which usually
implements the interface
Named . |
Named
This interface has to be implemented by all logic signature elements, which
are identified by their name.
|
Term
In contrast to the distinction of formulas and terms as made by most of the
inductive definitions of the syntax of a logic, an instance of this class can
stand for a term or a formula.
|
Class and Description |
---|
Name
A Name object is created to represent the name of an object which usually
implements the interface
Named . |
PosInOccurrence
This class describes a position in an occurrence of a term.
|
Class and Description |
---|
Namespace
A Namespace keeps track of already used
Name s and the objects
carrying these names. |
NamespaceSet |
Sequent
This class represents a sequent.
|
Term
In contrast to the distinction of formulas and terms as made by most of the
inductive definitions of the syntax of a logic, an instance of this class can
stand for a term or a formula.
|
Class and Description |
---|
Choice
A choice is an option in a category.
|
Namespace
A Namespace keeps track of already used
Name s and the objects
carrying these names. |
NamespaceSet |
Class and Description |
---|
Name
A Name object is created to represent the name of an object which usually
implements the interface
Named . |
PosInOccurrence
This class describes a position in an occurrence of a term.
|
Term
In contrast to the distinction of formulas and terms as made by most of the
inductive definitions of the syntax of a logic, an instance of this class can
stand for a term or a formula.
|
Class and Description |
---|
Sequent
This class represents a sequent.
|
Class and Description |
---|
PosInOccurrence
This class describes a position in an occurrence of a term.
|
Term
In contrast to the distinction of formulas and terms as made by most of the
inductive definitions of the syntax of a logic, an instance of this class can
stand for a term or a formula.
|
Class and Description |
---|
PosInOccurrence
This class describes a position in an occurrence of a term.
|
Class and Description |
---|
JavaBlock |
Sequent
This class represents a sequent.
|
SequentFormula
A sequent formula is a wrapper around a formula that occurs
as top level formula in a sequent.
|
Class and Description |
---|
PosInOccurrence
This class describes a position in an occurrence of a term.
|
Class and Description |
---|
Term
In contrast to the distinction of formulas and terms as made by most of the
inductive definitions of the syntax of a logic, an instance of this class can
stand for a term or a formula.
|
Class and Description |
---|
DefaultVisitor
This abstract Vistor class declares the interface for a common term visitor.
|
Term
In contrast to the distinction of formulas and terms as made by most of the
inductive definitions of the syntax of a logic, an instance of this class can
stand for a term or a formula.
|
Visitor |
Class and Description |
---|
Sequent
This class represents a sequent.
|
Class and Description |
---|
Term
In contrast to the distinction of formulas and terms as made by most of the
inductive definitions of the syntax of a logic, an instance of this class can
stand for a term or a formula.
|
Class and Description |
---|
Name
A Name object is created to represent the name of an object which usually
implements the interface
Named . |
Named
This interface has to be implemented by all logic signature elements, which
are identified by their name.
|
PosInOccurrence
This class describes a position in an occurrence of a term.
|
Class and Description |
---|
Named
This interface has to be implemented by all logic signature elements, which
are identified by their name.
|
Term
In contrast to the distinction of formulas and terms as made by most of the
inductive definitions of the syntax of a logic, an instance of this class can
stand for a term or a formula.
|
Class and Description |
---|
Term
In contrast to the distinction of formulas and terms as made by most of the
inductive definitions of the syntax of a logic, an instance of this class can
stand for a term or a formula.
|
Class and Description |
---|
Named
This interface has to be implemented by all logic signature elements, which
are identified by their name.
|
Sequent
This class represents a sequent.
|
Term
In contrast to the distinction of formulas and terms as made by most of the
inductive definitions of the syntax of a logic, an instance of this class can
stand for a term or a formula.
|
Class and Description |
---|
Term
In contrast to the distinction of formulas and terms as made by most of the
inductive definitions of the syntax of a logic, an instance of this class can
stand for a term or a formula.
|
Class and Description |
---|
Choice
A choice is an option in a category.
|
Name
A Name object is created to represent the name of an object which usually
implements the interface
Named . |
Named
This interface has to be implemented by all logic signature elements, which
are identified by their name.
|
Term
In contrast to the distinction of formulas and terms as made by most of the
inductive definitions of the syntax of a logic, an instance of this class can
stand for a term or a formula.
|
Class and Description |
---|
PosInOccurrence
This class describes a position in an occurrence of a term.
|
Semisequent
This class represents the succedent or antecendent part of a
sequent.
|
SequentChangeInfo
Records the changes made to a sequent.
|
Term
In contrast to the distinction of formulas and terms as made by most of the
inductive definitions of the syntax of a logic, an instance of this class can
stand for a term or a formula.
|
Class and Description |
---|
Term
In contrast to the distinction of formulas and terms as made by most of the
inductive definitions of the syntax of a logic, an instance of this class can
stand for a term or a formula.
|
TermBuilder
Use this class if you intend to build complex terms by hand.
|
Class and Description |
---|
JavaBlock |
Name
A Name object is created to represent the name of an object which usually
implements the interface
Named . |
Namespace
A Namespace keeps track of already used
Name s and the objects
carrying these names. |
NamespaceSet |
PosInOccurrence
This class describes a position in an occurrence of a term.
|
PosInProgram
this class describes the position of a statement in a program.
|
ProgramElementName |
ProgramPrefix
this interface is implemented by program elements that may be matched
by the inactive program prefix
|
Term
In contrast to the distinction of formulas and terms as made by most of the
inductive definitions of the syntax of a logic, an instance of this class can
stand for a term or a formula.
|
TermBuilder
Use this class if you intend to build complex terms by hand.
|
TermFactory
The TermFactory is the only way to create terms using constructors
of class Term or any of its subclasses.
|
TermServices
This interface defines the basic functionalities of services
required to construct
Term s. |
VariableNamer
Responsible for program variable naming issues.
|
Class and Description |
---|
Name
A Name object is created to represent the name of an object which usually
implements the interface
Named . |
ProgramElementName |
Class and Description |
---|
ProgramElementName |
Class and Description |
---|
Name
A Name object is created to represent the name of an object which usually
implements the interface
Named . |
Class and Description |
---|
Name
A Name object is created to represent the name of an object which usually
implements the interface
Named . |
Class and Description |
---|
Term
In contrast to the distinction of formulas and terms as made by most of the
inductive definitions of the syntax of a logic, an instance of this class can
stand for a term or a formula.
|
Class and Description |
---|
Namespace
A Namespace keeps track of already used
Name s and the objects
carrying these names. |
Class and Description |
---|
ProgramElementName |
Class and Description |
---|
PosInProgram
this class describes the position of a statement in a program.
|
ProgramElementName |
ProgramPrefix
this interface is implemented by program elements that may be matched
by the inactive program prefix
|
Class and Description |
---|
IntIterator
implemented by iterators of primitive type int
|
PosInProgram
this class describes the position of a statement in a program.
|
ProgramElementName |
Class and Description |
---|
Name
A Name object is created to represent the name of an object which usually
implements the interface
Named . |
Named
This interface has to be implemented by all logic signature elements, which
are identified by their name.
|
Namespace
A Namespace keeps track of already used
Name s and the objects
carrying these names. |
Term
In contrast to the distinction of formulas and terms as made by most of the
inductive definitions of the syntax of a logic, an instance of this class can
stand for a term or a formula.
|
TermServices
This interface defines the basic functionalities of services
required to construct
Term s. |
Class and Description |
---|
BoundVariableTools
Some generally useful tools for dealing with arrays of bound variables
|
Choice
A choice is an option in a category.
|
ClashFreeSubst |
DefaultVisitor
This abstract Vistor class declares the interface for a common term visitor.
|
FormulaChangeInfo
This class is used to hold information about modified formulas.
|
IntIterator
implemented by iterators of primitive type int
|
JavaBlock |
Name
A Name object is created to represent the name of an object which usually
implements the interface
Named . |
NameCreationInfo |
Named
This interface has to be implemented by all logic signature elements, which
are identified by their name.
|
Namespace
A Namespace keeps track of already used
Name s and the objects
carrying these names. |
NamespaceSet |
PIOPathIterator
This interface represents an iterator, iterating the nodes on the
path between the root of a term and a position within the term,
given by a
PosInOccurrence -object |
PosInOccurrence
This class describes a position in an occurrence of a term.
|
PosInProgram
this class describes the position of a statement in a program.
|
PosInTerm
Describes the position within a term by a sequence of integers.
|
ProgramElementName |
ProgramPrefix
this interface is implemented by program elements that may be matched
by the inactive program prefix
|
RenameTable |
RenamingTable |
Semisequent
This class represents the succedent or antecendent part of a
sequent.
|
SemisequentChangeInfo
Records the changes made to a semisequent.
|
Sequent
This class represents a sequent.
|
SequentChangeInfo
Records the changes made to a sequent.
|
SequentFormula
A sequent formula is a wrapper around a formula that occurs
as top level formula in a sequent.
|
Sorted |
Term
In contrast to the distinction of formulas and terms as made by most of the
inductive definitions of the syntax of a logic, an instance of this class can
stand for a term or a formula.
|
TermBuilder
Use this class if you intend to build complex terms by hand.
|
TermFactory
The TermFactory is the only way to create terms using constructors
of class Term or any of its subclasses.
|
TermOrdering
Interface for term ordering
|
TermServices
This interface defines the basic functionalities of services
required to construct
Term s. |
VariableNamer
Responsible for program variable naming issues.
|
VariableNamer.BasenameAndIndex
tuple of a basename and an index
|
Visitor |
Class and Description |
---|
JavaBlock |
Name
A Name object is created to represent the name of an object which usually
implements the interface
Named . |
Named
This interface has to be implemented by all logic signature elements, which
are identified by their name.
|
PosInOccurrence
This class describes a position in an occurrence of a term.
|
Semisequent
This class represents the succedent or antecendent part of a
sequent.
|
Sequent
This class represents a sequent.
|
SequentChangeInfo
Records the changes made to a sequent.
|
SequentFormula
A sequent formula is a wrapper around a formula that occurs
as top level formula in a sequent.
|
Term
In contrast to the distinction of formulas and terms as made by most of the
inductive definitions of the syntax of a logic, an instance of this class can
stand for a term or a formula.
|
TermFactory
The TermFactory is the only way to create terms using constructors
of class Term or any of its subclasses.
|
TermServices
This interface defines the basic functionalities of services
required to construct
Term s. |
Class and Description |
---|
Name
A Name object is created to represent the name of an object which usually
implements the interface
Named . |
Named
This interface has to be implemented by all logic signature elements, which
are identified by their name.
|
PosInOccurrence
This class describes a position in an occurrence of a term.
|
ProgramConstruct
A type that implement this interface can be used in all java
programs instead of an expression or statement.
|
ProgramElementName |
ProgramInLogic
represents something in logic that originates from a program like
queries, program variables and therefore has a KeYJavaType
|
Sorted |
Term
In contrast to the distinction of formulas and terms as made by most of the
inductive definitions of the syntax of a logic, an instance of this class can
stand for a term or a formula.
|
TermBuilder
Use this class if you intend to build complex terms by hand.
|
TermCreationException |
TermServices
This interface defines the basic functionalities of services
required to construct
Term s. |
Class and Description |
---|
Name
A Name object is created to represent the name of an object which usually
implements the interface
Named . |
Named
This interface has to be implemented by all logic signature elements, which
are identified by their name.
|
Term
In contrast to the distinction of formulas and terms as made by most of the
inductive definitions of the syntax of a logic, an instance of this class can
stand for a term or a formula.
|
TermServices
This interface defines the basic functionalities of services
required to construct
Term s. |
Class and Description |
---|
Term
In contrast to the distinction of formulas and terms as made by most of the
inductive definitions of the syntax of a logic, an instance of this class can
stand for a term or a formula.
|
TermServices
This interface defines the basic functionalities of services
required to construct
Term s. |
Class and Description |
---|
Name
A Name object is created to represent the name of an object which usually
implements the interface
Named . |
Named
This interface has to be implemented by all logic signature elements, which
are identified by their name.
|
PosInOccurrence
This class describes a position in an occurrence of a term.
|
Class and Description |
---|
PosInOccurrence
This class describes a position in an occurrence of a term.
|
Sequent
This class represents a sequent.
|
SequentFormula
A sequent formula is a wrapper around a formula that occurs
as top level formula in a sequent.
|
Term
In contrast to the distinction of formulas and terms as made by most of the
inductive definitions of the syntax of a logic, an instance of this class can
stand for a term or a formula.
|
Class and Description |
---|
Choice
A choice is an option in a category.
|
Namespace
A Namespace keeps track of already used
Name s and the objects
carrying these names. |
NamespaceSet |
Sequent
This class represents a sequent.
|
Term
In contrast to the distinction of formulas and terms as made by most of the
inductive definitions of the syntax of a logic, an instance of this class can
stand for a term or a formula.
|
Class and Description |
---|
Choice
A choice is an option in a category.
|
Name
A Name object is created to represent the name of an object which usually
implements the interface
Named . |
Named
This interface has to be implemented by all logic signature elements, which
are identified by their name.
|
Namespace
A Namespace keeps track of already used
Name s and the objects
carrying these names. |
NamespaceSet |
Semisequent
This class represents the succedent or antecendent part of a
sequent.
|
Sequent
This class represents a sequent.
|
Term
In contrast to the distinction of formulas and terms as made by most of the
inductive definitions of the syntax of a logic, an instance of this class can
stand for a term or a formula.
|
TermFactory
The TermFactory is the only way to create terms using constructors
of class Term or any of its subclasses.
|
Class and Description |
---|
Namespace
A Namespace keeps track of already used
Name s and the objects
carrying these names. |
NamespaceSet |
Sequent
This class represents a sequent.
|
Term
In contrast to the distinction of formulas and terms as made by most of the
inductive definitions of the syntax of a logic, an instance of this class can
stand for a term or a formula.
|
Class and Description |
---|
JavaBlock |
Name
A Name object is created to represent the name of an object which usually
implements the interface
Named . |
PosInOccurrence
This class describes a position in an occurrence of a term.
|
Semisequent
This class represents the succedent or antecendent part of a
sequent.
|
Sequent
This class represents a sequent.
|
SequentFormula
A sequent formula is a wrapper around a formula that occurs
as top level formula in a sequent.
|
Term
In contrast to the distinction of formulas and terms as made by most of the
inductive definitions of the syntax of a logic, an instance of this class can
stand for a term or a formula.
|
Class and Description |
---|
DefaultVisitor
This abstract Vistor class declares the interface for a common term visitor.
|
FormulaChangeInfo
This class is used to hold information about modified formulas.
|
Name
A Name object is created to represent the name of an object which usually
implements the interface
Named . |
Named
This interface has to be implemented by all logic signature elements, which
are identified by their name.
|
NamespaceSet |
PosInOccurrence
This class describes a position in an occurrence of a term.
|
RenamingTable |
Semisequent
This class represents the succedent or antecendent part of a
sequent.
|
SemisequentChangeInfo
Records the changes made to a semisequent.
|
Sequent
This class represents a sequent.
|
SequentChangeInfo
Records the changes made to a sequent.
|
SequentFormula
A sequent formula is a wrapper around a formula that occurs
as top level formula in a sequent.
|
Term
In contrast to the distinction of formulas and terms as made by most of the
inductive definitions of the syntax of a logic, an instance of this class can
stand for a term or a formula.
|
TermFactory
The TermFactory is the only way to create terms using constructors
of class Term or any of its subclasses.
|
TermServices
This interface defines the basic functionalities of services
required to construct
Term s. |
Visitor |
Class and Description |
---|
Term
In contrast to the distinction of formulas and terms as made by most of the
inductive definitions of the syntax of a logic, an instance of this class can
stand for a term or a formula.
|
Class and Description |
---|
Choice
A choice is an option in a category.
|
JavaBlock |
Name
A Name object is created to represent the name of an object which usually
implements the interface
Named . |
Namespace
A Namespace keeps track of already used
Name s and the objects
carrying these names. |
NamespaceSet |
Term
In contrast to the distinction of formulas and terms as made by most of the
inductive definitions of the syntax of a logic, an instance of this class can
stand for a term or a formula.
|
TermBuilder
Use this class if you intend to build complex terms by hand.
|
Class and Description |
---|
Namespace
A Namespace keeps track of already used
Name s and the objects
carrying these names. |
PosInOccurrence
This class describes a position in an occurrence of a term.
|
PosInTerm
Describes the position within a term by a sequence of integers.
|
Sequent
This class represents a sequent.
|
Term
In contrast to the distinction of formulas and terms as made by most of the
inductive definitions of the syntax of a logic, an instance of this class can
stand for a term or a formula.
|
Class and Description |
---|
Name
A Name object is created to represent the name of an object which usually
implements the interface
Named . |
PosInTerm
Describes the position within a term by a sequence of integers.
|
Class and Description |
---|
PosInOccurrence
This class describes a position in an occurrence of a term.
|
Sequent
This class represents a sequent.
|
SequentFormula
A sequent formula is a wrapper around a formula that occurs
as top level formula in a sequent.
|
Term
In contrast to the distinction of formulas and terms as made by most of the
inductive definitions of the syntax of a logic, an instance of this class can
stand for a term or a formula.
|
Class and Description |
---|
Term
In contrast to the distinction of formulas and terms as made by most of the
inductive definitions of the syntax of a logic, an instance of this class can
stand for a term or a formula.
|
TermServices
This interface defines the basic functionalities of services
required to construct
Term s. |
Class and Description |
---|
PosInOccurrence
This class describes a position in an occurrence of a term.
|
SequentChangeInfo
Records the changes made to a sequent.
|
Class and Description |
---|
Choice
A choice is an option in a category.
|
DefaultVisitor
This abstract Vistor class declares the interface for a common term visitor.
|
JavaBlock |
Name
A Name object is created to represent the name of an object which usually
implements the interface
Named . |
Named
This interface has to be implemented by all logic signature elements, which
are identified by their name.
|
Namespace
A Namespace keeps track of already used
Name s and the objects
carrying these names. |
NamespaceSet |
PosInOccurrence
This class describes a position in an occurrence of a term.
|
RenameTable |
Semisequent
This class represents the succedent or antecendent part of a
sequent.
|
Sequent
This class represents a sequent.
|
SequentFormula
A sequent formula is a wrapper around a formula that occurs
as top level formula in a sequent.
|
Term
In contrast to the distinction of formulas and terms as made by most of the
inductive definitions of the syntax of a logic, an instance of this class can
stand for a term or a formula.
|
TermBuilder
Use this class if you intend to build complex terms by hand.
|
TermFactory
The TermFactory is the only way to create terms using constructors
of class Term or any of its subclasses.
|
TermServices
This interface defines the basic functionalities of services
required to construct
Term s. |
Visitor |
Class and Description |
---|
Term
In contrast to the distinction of formulas and terms as made by most of the
inductive definitions of the syntax of a logic, an instance of this class can
stand for a term or a formula.
|
TermServices
This interface defines the basic functionalities of services
required to construct
Term s. |
Class and Description |
---|
PosInOccurrence
This class describes a position in an occurrence of a term.
|
Semisequent
This class represents the succedent or antecendent part of a
sequent.
|
Sequent
This class represents a sequent.
|
SequentChangeInfo
Records the changes made to a sequent.
|
SequentFormula
A sequent formula is a wrapper around a formula that occurs
as top level formula in a sequent.
|
Term
In contrast to the distinction of formulas and terms as made by most of the
inductive definitions of the syntax of a logic, an instance of this class can
stand for a term or a formula.
|
Class and Description |
---|
Name
A Name object is created to represent the name of an object which usually
implements the interface
Named . |
PosInProgram
this class describes the position of a statement in a program.
|
Term
In contrast to the distinction of formulas and terms as made by most of the
inductive definitions of the syntax of a logic, an instance of this class can
stand for a term or a formula.
|
TermServices
This interface defines the basic functionalities of services
required to construct
Term s. |
Class and Description |
---|
JavaBlock |
Name
A Name object is created to represent the name of an object which usually
implements the interface
Named . |
PosInOccurrence
This class describes a position in an occurrence of a term.
|
SequentFormula
A sequent formula is a wrapper around a formula that occurs
as top level formula in a sequent.
|
Term
In contrast to the distinction of formulas and terms as made by most of the
inductive definitions of the syntax of a logic, an instance of this class can
stand for a term or a formula.
|
TermServices
This interface defines the basic functionalities of services
required to construct
Term s. |
Class and Description |
---|
Term
In contrast to the distinction of formulas and terms as made by most of the
inductive definitions of the syntax of a logic, an instance of this class can
stand for a term or a formula.
|
Class and Description |
---|
Term
In contrast to the distinction of formulas and terms as made by most of the
inductive definitions of the syntax of a logic, an instance of this class can
stand for a term or a formula.
|
Class and Description |
---|
Term
In contrast to the distinction of formulas and terms as made by most of the
inductive definitions of the syntax of a logic, an instance of this class can
stand for a term or a formula.
|
Class and Description |
---|
Name
A Name object is created to represent the name of an object which usually
implements the interface
Named . |
PosInOccurrence
This class describes a position in an occurrence of a term.
|
Term
In contrast to the distinction of formulas and terms as made by most of the
inductive definitions of the syntax of a logic, an instance of this class can
stand for a term or a formula.
|
TermServices
This interface defines the basic functionalities of services
required to construct
Term s. |
Class and Description |
---|
Term
In contrast to the distinction of formulas and terms as made by most of the
inductive definitions of the syntax of a logic, an instance of this class can
stand for a term or a formula.
|
Class and Description |
---|
JavaBlock |
Name
A Name object is created to represent the name of an object which usually
implements the interface
Named . |
Named
This interface has to be implemented by all logic signature elements, which
are identified by their name.
|
PosInOccurrence
This class describes a position in an occurrence of a term.
|
ProgramElementName |
Sequent
This class represents a sequent.
|
Sorted |
Term
In contrast to the distinction of formulas and terms as made by most of the
inductive definitions of the syntax of a logic, an instance of this class can
stand for a term or a formula.
|
TermServices
This interface defines the basic functionalities of services
required to construct
Term s. |
Class and Description |
---|
Name
A Name object is created to represent the name of an object which usually
implements the interface
Named . |
Named
This interface has to be implemented by all logic signature elements, which
are identified by their name.
|
Sorted |
Term
In contrast to the distinction of formulas and terms as made by most of the
inductive definitions of the syntax of a logic, an instance of this class can
stand for a term or a formula.
|
Class and Description |
---|
Choice
A choice is an option in a category.
|
Name
A Name object is created to represent the name of an object which usually
implements the interface
Named . |
Sequent
This class represents a sequent.
|
Term
In contrast to the distinction of formulas and terms as made by most of the
inductive definitions of the syntax of a logic, an instance of this class can
stand for a term or a formula.
|
TermServices
This interface defines the basic functionalities of services
required to construct
Term s. |
Class and Description |
---|
Choice
A choice is an option in a category.
|
Name
A Name object is created to represent the name of an object which usually
implements the interface
Named . |
Namespace
A Namespace keeps track of already used
Name s and the objects
carrying these names. |
Class and Description |
---|
Name
A Name object is created to represent the name of an object which usually
implements the interface
Named . |
PosInOccurrence
This class describes a position in an occurrence of a term.
|
Sequent
This class represents a sequent.
|
Term
In contrast to the distinction of formulas and terms as made by most of the
inductive definitions of the syntax of a logic, an instance of this class can
stand for a term or a formula.
|
TermServices
This interface defines the basic functionalities of services
required to construct
Term s. |
Class and Description |
---|
Sequent
This class represents a sequent.
|
Class and Description |
---|
Sequent
This class represents a sequent.
|
Term
In contrast to the distinction of formulas and terms as made by most of the
inductive definitions of the syntax of a logic, an instance of this class can
stand for a term or a formula.
|
Class and Description |
---|
Sequent
This class represents a sequent.
|
Class and Description |
---|
Name
A Name object is created to represent the name of an object which usually
implements the interface
Named . |
SequentFormula
A sequent formula is a wrapper around a formula that occurs
as top level formula in a sequent.
|
Term
In contrast to the distinction of formulas and terms as made by most of the
inductive definitions of the syntax of a logic, an instance of this class can
stand for a term or a formula.
|
TermBuilder
Use this class if you intend to build complex terms by hand.
|
TermServices
This interface defines the basic functionalities of services
required to construct
Term s. |
Class and Description |
---|
Term
In contrast to the distinction of formulas and terms as made by most of the
inductive definitions of the syntax of a logic, an instance of this class can
stand for a term or a formula.
|
Class and Description |
---|
Name
A Name object is created to represent the name of an object which usually
implements the interface
Named . |
Class and Description |
---|
Term
In contrast to the distinction of formulas and terms as made by most of the
inductive definitions of the syntax of a logic, an instance of this class can
stand for a term or a formula.
|
TermBuilder
Use this class if you intend to build complex terms by hand.
|
Class and Description |
---|
Term
In contrast to the distinction of formulas and terms as made by most of the
inductive definitions of the syntax of a logic, an instance of this class can
stand for a term or a formula.
|
TermBuilder
Use this class if you intend to build complex terms by hand.
|
TermServices
This interface defines the basic functionalities of services
required to construct
Term s. |
Class and Description |
---|
Term
In contrast to the distinction of formulas and terms as made by most of the
inductive definitions of the syntax of a logic, an instance of this class can
stand for a term or a formula.
|
TermBuilder
Use this class if you intend to build complex terms by hand.
|
Class and Description |
---|
Name
A Name object is created to represent the name of an object which usually
implements the interface
Named . |
Named
This interface has to be implemented by all logic signature elements, which
are identified by their name.
|
PosInOccurrence
This class describes a position in an occurrence of a term.
|
PosInTerm
Describes the position within a term by a sequence of integers.
|
Sequent
This class represents a sequent.
|
Term
In contrast to the distinction of formulas and terms as made by most of the
inductive definitions of the syntax of a logic, an instance of this class can
stand for a term or a formula.
|
Class and Description |
---|
Name
A Name object is created to represent the name of an object which usually
implements the interface
Named . |
PosInOccurrence
This class describes a position in an occurrence of a term.
|
Semisequent
This class represents the succedent or antecendent part of a
sequent.
|
SequentFormula
A sequent formula is a wrapper around a formula that occurs
as top level formula in a sequent.
|
Term
In contrast to the distinction of formulas and terms as made by most of the
inductive definitions of the syntax of a logic, an instance of this class can
stand for a term or a formula.
|
Class and Description |
---|
PosInOccurrence
This class describes a position in an occurrence of a term.
|
Class and Description |
---|
Name
A Name object is created to represent the name of an object which usually
implements the interface
Named . |
PosInOccurrence
This class describes a position in an occurrence of a term.
|
Class and Description |
---|
BooleanContainer
BooleanContainer wraps primitive bool
|
DefaultVisitor
This abstract Vistor class declares the interface for a common term visitor.
|
Name
A Name object is created to represent the name of an object which usually
implements the interface
Named . |
Named
This interface has to be implemented by all logic signature elements, which
are identified by their name.
|
PosInOccurrence
This class describes a position in an occurrence of a term.
|
Sorted |
Term
In contrast to the distinction of formulas and terms as made by most of the
inductive definitions of the syntax of a logic, an instance of this class can
stand for a term or a formula.
|
TermServices
This interface defines the basic functionalities of services
required to construct
Term s. |
Visitor |
Class and Description |
---|
Name
A Name object is created to represent the name of an object which usually
implements the interface
Named . |
PosInOccurrence
This class describes a position in an occurrence of a term.
|
PosInTerm
Describes the position within a term by a sequence of integers.
|
Term
In contrast to the distinction of formulas and terms as made by most of the
inductive definitions of the syntax of a logic, an instance of this class can
stand for a term or a formula.
|
Class and Description |
---|
Name
A Name object is created to represent the name of an object which usually
implements the interface
Named . |
PosInOccurrence
This class describes a position in an occurrence of a term.
|
Term
In contrast to the distinction of formulas and terms as made by most of the
inductive definitions of the syntax of a logic, an instance of this class can
stand for a term or a formula.
|
Class and Description |
---|
PosInOccurrence
This class describes a position in an occurrence of a term.
|
SequentFormula
A sequent formula is a wrapper around a formula that occurs
as top level formula in a sequent.
|
Term
In contrast to the distinction of formulas and terms as made by most of the
inductive definitions of the syntax of a logic, an instance of this class can
stand for a term or a formula.
|
TermServices
This interface defines the basic functionalities of services
required to construct
Term s. |
Class and Description |
---|
Name
A Name object is created to represent the name of an object which usually
implements the interface
Named . |
PosInOccurrence
This class describes a position in an occurrence of a term.
|
Sequent
This class represents a sequent.
|
SequentFormula
A sequent formula is a wrapper around a formula that occurs
as top level formula in a sequent.
|
Term
In contrast to the distinction of formulas and terms as made by most of the
inductive definitions of the syntax of a logic, an instance of this class can
stand for a term or a formula.
|
TermBuilder
Use this class if you intend to build complex terms by hand.
|
Class and Description |
---|
PosInOccurrence
This class describes a position in an occurrence of a term.
|
Term
In contrast to the distinction of formulas and terms as made by most of the
inductive definitions of the syntax of a logic, an instance of this class can
stand for a term or a formula.
|
Class and Description |
---|
PosInOccurrence
This class describes a position in an occurrence of a term.
|
Term
In contrast to the distinction of formulas and terms as made by most of the
inductive definitions of the syntax of a logic, an instance of this class can
stand for a term or a formula.
|
TermBuilder
Use this class if you intend to build complex terms by hand.
|
Class and Description |
---|
Term
In contrast to the distinction of formulas and terms as made by most of the
inductive definitions of the syntax of a logic, an instance of this class can
stand for a term or a formula.
|
Class and Description |
---|
Term
In contrast to the distinction of formulas and terms as made by most of the
inductive definitions of the syntax of a logic, an instance of this class can
stand for a term or a formula.
|
Class and Description |
---|
Term
In contrast to the distinction of formulas and terms as made by most of the
inductive definitions of the syntax of a logic, an instance of this class can
stand for a term or a formula.
|
Class and Description |
---|
Name
A Name object is created to represent the name of an object which usually
implements the interface
Named . |
PosInOccurrence
This class describes a position in an occurrence of a term.
|
Sequent
This class represents a sequent.
|
SequentFormula
A sequent formula is a wrapper around a formula that occurs
as top level formula in a sequent.
|
Term
In contrast to the distinction of formulas and terms as made by most of the
inductive definitions of the syntax of a logic, an instance of this class can
stand for a term or a formula.
|
TermServices
This interface defines the basic functionalities of services
required to construct
Term s. |
Class and Description |
---|
Sequent
This class represents a sequent.
|
Term
In contrast to the distinction of formulas and terms as made by most of the
inductive definitions of the syntax of a logic, an instance of this class can
stand for a term or a formula.
|
Class and Description |
---|
Name
A Name object is created to represent the name of an object which usually
implements the interface
Named . |
Named
This interface has to be implemented by all logic signature elements, which
are identified by their name.
|
PosInOccurrence
This class describes a position in an occurrence of a term.
|
SequentFormula
A sequent formula is a wrapper around a formula that occurs
as top level formula in a sequent.
|
Term
In contrast to the distinction of formulas and terms as made by most of the
inductive definitions of the syntax of a logic, an instance of this class can
stand for a term or a formula.
|
Class and Description |
---|
Term
In contrast to the distinction of formulas and terms as made by most of the
inductive definitions of the syntax of a logic, an instance of this class can
stand for a term or a formula.
|
Class and Description |
---|
DefaultVisitor
This abstract Vistor class declares the interface for a common term visitor.
|
Name
A Name object is created to represent the name of an object which usually
implements the interface
Named . |
PosInOccurrence
This class describes a position in an occurrence of a term.
|
PosInTerm
Describes the position within a term by a sequence of integers.
|
Semisequent
This class represents the succedent or antecendent part of a
sequent.
|
Sequent
This class represents a sequent.
|
SequentFormula
A sequent formula is a wrapper around a formula that occurs
as top level formula in a sequent.
|
Term
In contrast to the distinction of formulas and terms as made by most of the
inductive definitions of the syntax of a logic, an instance of this class can
stand for a term or a formula.
|
TermFactory
The TermFactory is the only way to create terms using constructors
of class Term or any of its subclasses.
|
Visitor |
Class and Description |
---|
DefaultVisitor
This abstract Vistor class declares the interface for a common term visitor.
|
Sequent
This class represents a sequent.
|
Term
In contrast to the distinction of formulas and terms as made by most of the
inductive definitions of the syntax of a logic, an instance of this class can
stand for a term or a formula.
|
TermServices
This interface defines the basic functionalities of services
required to construct
Term s. |
Visitor |
Class and Description |
---|
Name
A Name object is created to represent the name of an object which usually
implements the interface
Named . |
Term
In contrast to the distinction of formulas and terms as made by most of the
inductive definitions of the syntax of a logic, an instance of this class can
stand for a term or a formula.
|
TermServices
This interface defines the basic functionalities of services
required to construct
Term s. |
Class and Description |
---|
Name
A Name object is created to represent the name of an object which usually
implements the interface
Named . |
Named
This interface has to be implemented by all logic signature elements, which
are identified by their name.
|
NamespaceSet |
TermServices
This interface defines the basic functionalities of services
required to construct
Term s. |
Class and Description |
---|
JavaBlock |
Sequent
This class represents a sequent.
|
Term
In contrast to the distinction of formulas and terms as made by most of the
inductive definitions of the syntax of a logic, an instance of this class can
stand for a term or a formula.
|
Class and Description |
---|
Term
In contrast to the distinction of formulas and terms as made by most of the
inductive definitions of the syntax of a logic, an instance of this class can
stand for a term or a formula.
|
Class and Description |
---|
PosInOccurrence
This class describes a position in an occurrence of a term.
|
Class and Description |
---|
Choice
A choice is an option in a category.
|
Name
A Name object is created to represent the name of an object which usually
implements the interface
Named . |
Sequent
This class represents a sequent.
|
Sorted |
Term
In contrast to the distinction of formulas and terms as made by most of the
inductive definitions of the syntax of a logic, an instance of this class can
stand for a term or a formula.
|
TermBuilder
Use this class if you intend to build complex terms by hand.
|
Class and Description |
---|
JavaBlock |
Name
A Name object is created to represent the name of an object which usually
implements the interface
Named . |
NamespaceSet |
PosInOccurrence
This class describes a position in an occurrence of a term.
|
Sequent
This class represents a sequent.
|
Term
In contrast to the distinction of formulas and terms as made by most of the
inductive definitions of the syntax of a logic, an instance of this class can
stand for a term or a formula.
|
Class and Description |
---|
PosInOccurrence
This class describes a position in an occurrence of a term.
|
Term
In contrast to the distinction of formulas and terms as made by most of the
inductive definitions of the syntax of a logic, an instance of this class can
stand for a term or a formula.
|
Class and Description |
---|
PosInOccurrence
This class describes a position in an occurrence of a term.
|
Class and Description |
---|
PosInOccurrence
This class describes a position in an occurrence of a term.
|
Copyright © 2003-2019 The KeY-Project.