Package | Description |
---|---|
de.uka.ilkd.key.informationflow.macros |
Class and Description |
---|
AbstractFinishAuxiliaryComputationMacro |
ExhaustiveProofMacro
The abstract class ExhaustiveProofMacro can be used to create compound macros
which either apply the macro given by
ExhaustiveProofMacro.getProofMacro() directly, or
--if not directly applicable-- search on the sequent for any applicable
posInOcc and apply it on the first applicable one or --if not applicable
anywhere on the sequent-- do not apply it. |
StartSideProofMacro |
UseInformationFlowContractMacro.PropExpansionStrategy
This strategy accepts all rule apps for which the rule name starts with a
string in the admitted set and rejects everything else.
|
Copyright © 2003-2019 The KeY-Project.