| 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. |