de.uka.ilkd.key.strategy.termProjection |
|
Java Source File Name | Type | Comment |
AbstractDividePolynomialsProjection.java | Class | |
AssumptionProjection.java | Class | Term projection that delivers the assumptions of a taclet application
(the formulas that the \assumes clause of the taclet refers to). |
CoeffGcdProjection.java | Class | Given a monomial and a polynomial, this projection computes the gcd of all
numerical coefficients. |
DividePolynomialsProjection.java | Class | |
FocusFormulaProjection.java | Class | |
FocusProjection.java | Class | Projection of a rule application to its focus (the term or formula that the
rule operates on, that for taclets is described using \find ,
and that can be modified by the rule). |
MonomialColumnOp.java | Class | |
ProjectionToTerm.java | Interface | Interface for mappings from rule applications to terms. |
ReduceMonomialsProjection.java | Class | Projection for dividing one monomial by another. |
SubtermProjection.java | Class | Projection for computing a subterm of a given term. |
SVInstantiationProjection.java | Class | Projection of taclet apps to the instantiation of a schema variable. |
TermBuffer.java | Class | Projection that can store and returns an arbitrary term or formula. |
TermConstructionProjection.java | Class | Term projection for constructing a bigger term from a sequence of direct
subterms and an operator. |