Package | Description |
---|---|
de.uka.ilkd.key.informationflow.macros | |
de.uka.ilkd.key.macros |
Modifier and Type | Class and Description |
---|---|
class |
FullUseInformationFlowContractMacro |
class |
StateExpansionAndInfFlowContractApplicationMacro |
Modifier and Type | Class and Description |
---|---|
class |
FullAutoPilotProofMacro
This class captures a proof macro which is meant to fully automise KeY proof
workflow.
|
class |
SequentialOnLastGoalProofMacro |
class |
SMTPreparationMacro
A macro that performs all simplifications that are necessary in order to perform a translation
of the sequent to SMT.
|
Copyright © 2003-2019 The KeY-Project.