| java.lang.Object
 de.uka.ilkd.key.rule.NewDependingOn
| NewDependingOn | | public class NewDependingOn (Code) | | class containing a pair of SchemaVariables, the first one being a
TermSV, the second one a FormulaSV, representing a "c new depending
on phi" statement within a varcond of a taclet
|
| NewDependingOn | | public NewDependingOn(SchemaVariable first, SchemaVariable second)(Code) | | constructs a pair of variables given two SchemaVariables. The first SchemaVariable
has to occur bound in the Taclet, while the second one can stand for a
an arbitrary term of formula, in order to model a pair of the not-free-in relation of
an Taclet.
|
| first | | public SchemaVariable first()(Code) | | returns the first SchemaVariable of the pair. This
SchemaVariable has to be matched to a QuantifiableVariable
|
| hashCode | | public int hashCode()(Code) | | |
|
|