Package | Description |
---|---|
de.uka.ilkd.key.taclettranslation.assumptions | |
de.uka.ilkd.key.taclettranslation.lemma |
Modifier and Type | Class and Description |
---|---|
class |
AssumptionGenerator |
Modifier and Type | Interface and Description |
---|---|
interface |
LemmaGenerator
A Lemma Generator translates a taclet to its corresponding
first order logic formula thats validity implies the validity
of the taclet.
|
Modifier and Type | Class and Description |
---|---|
class |
GenericRemovingLemmaGenerator
Generic removing lemma generator adds the default implementation only that all
GenericSort s are replaced to equally named ProxySort s. |
Copyright © 2003-2019 The KeY-Project.