| java.lang.Object
 de.uka.ilkd.key.rule.TacletGoalTemplate
de.uka.ilkd.key.rule.RewriteTacletGoalTemplate
| RewriteTacletGoalTemplate | | public class RewriteTacletGoalTemplate extends TacletGoalTemplate (Code) | | this class inherits from TacletGoalTemplate. It is used if there is a
replacewith in the ruleGoals that replaces a term by another
term. For a sequent
See Also: de.uka.ilkd.key.proof.AnteSuccTacletGoalTemplate |
| RewriteTacletGoalTemplate | | public RewriteTacletGoalTemplate(Sequent addedSeq, ListOfTaclet addedRules, Term 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 Term that replaces another one |
| RewriteTacletGoalTemplate | | public RewriteTacletGoalTemplate(Sequent addedSeq, ListOfTaclet addedRules, Term 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 Term replaceWith()(Code) | | a Taclet may replace a Term by another. The new Term is returned.
Term being paramter in the rule goal replacewith(Seq) |
| replaceWithExpressionAsObject | | Object replaceWithExpressionAsObject()(Code) | | Term being paramter in the rule goal replacewith(term) |
|
|