| java.lang.Object de.uka.ilkd.key.rule.TacletGoalTemplate de.uka.ilkd.key.rule.AntecSuccTacletGoalTemplate
AntecSuccTacletGoalTemplate | public AntecSuccTacletGoalTemplate(Sequent addedSeq, ListOfTaclet addedRules, Sequent replacewith, SetOfSchemaVariable pvs)(Code) | | creates new Goaldescription
Parameters: addedSeq - new Sequent to be added Parameters: addedRules - ListOfTaclet contains the new allowed rulesat this branch Parameters: ruleVars - ListOfRulevariable contains used rulevariables Parameters: replacewith - the Sequent that replaces another one |
AntecSuccTacletGoalTemplate | public AntecSuccTacletGoalTemplate(Sequent addedSeq, ListOfTaclet addedRules, Sequent replacewith)(Code) | | |
getBoundVariables | protected SetOfQuantifiableVariable getBoundVariables()(Code) | | rertieves and returns all variables that are bound in the
goal template
all variables that occur bound in this goal template |
hashCode | public int hashCode()(Code) | | |
replaceWith | public Sequent replaceWith()(Code) | | a Taclet may replace a Sequent by another. The new Sequent is returned.
this Sequent.
Sequent being paramter in the rule goal replacewith(Seq) |
replaceWithExpressionAsObject | Object replaceWithExpressionAsObject()(Code) | | Sequent being paramter in the rule goal replacewith(Seq) |
|
|