Modifier and Type | Method and Description |
---|---|
static java.util.List<java.util.List<java.lang.String>> |
InstantiationFileHandler.getInstantiationListsFor(Taclet taclet) |
static boolean |
InstantiationFileHandler.hasInstantiationListsFor(Taclet taclet) |
boolean |
AbstractProofControl.selectedTaclet(Taclet taclet,
Goal goal,
PosInOccurrence pos) |
boolean |
ProofControl.selectedTaclet(Taclet taclet,
Goal goal,
PosInOccurrence pos) |
Modifier and Type | Method and Description |
---|---|
Taclet |
TacletInstantiationModel.taclet() |
Modifier and Type | Method and Description |
---|---|
ImmutableSet<Taclet> |
LemmataHandler.filter(java.util.List<TacletSoundnessPOLoader.TacletInfo> taclets) |
ImmutableSet<Taclet> |
LemmaSelectionDialog.filter(java.util.List<TacletSoundnessPOLoader.TacletInfo> taclets) |
ImmutableSet<Taclet> |
LemmaSelectionDialog.showModal(java.util.List<TacletSoundnessPOLoader.TacletInfo> taclets) |
Modifier and Type | Method and Description |
---|---|
protected Sequent |
InsertHiddenTacletMenuItem.checkTaclet(Taclet t)
determines the sequent with the formulas to be added
or null if the given taclet is not thought to be displayed
by this component
|
protected Sequent |
InsertSystemInvariantTacletMenuItem.checkTaclet(Taclet t)
determines the sequent with the formulas to be added
or null if the given taclet is not thought to be displayed
by this component
|
protected abstract Sequent |
InsertionTacletBrowserMenuItem.checkTaclet(Taclet t) |
boolean |
InsertionTacletBrowserMenuItem.isResponsible(Taclet t)
tests if this class is responsible for the given taclet
|
boolean |
DragNDropInstantiator.TacletFilter.satisfiesFilterCondition(Taclet taclet)
checks if the taclet satisfies certain syntactic criterias
|
boolean |
DragNDropInstantiator.TacletFilter.TacletWithIfFindAndReplacewith.satisfiesFilterCondition(Taclet taclet)
tests if the given taclet consists of an assumes,
find and replacewith part and returns true
if the test is positive
|
boolean |
DragNDropInstantiator.TacletFilter.TacletWithIfFindAndNoReplacewith.satisfiesFilterCondition(Taclet taclet)
tests if the given taclet consists of an assumes,
find and no replacewith part and
returns true if the test is positive
|
boolean |
DragNDropInstantiator.TacletFilter.TacletWithNoIfFindAndAddrule.satisfiesFilterCondition(Taclet taclet)
tests if the given taclet consists of an assume,
find and no replacewith part and
returns true if the test is positive
|
boolean |
DragNDropInstantiator.TacletFilter.TacletWithNoIf.satisfiesFilterCondition(Taclet taclet)
checks if the taclet has a find part and no assumes sequent
|
Modifier and Type | Method and Description |
---|---|
void |
InfFlowProof.addGoalTemplates(Taclet t) |
Modifier and Type | Class and Description |
---|---|
class |
InfFlowContractAppTaclet
A normal RewriteTaclet except that the formula which is added by this taclet
is also added to the list of formulas contained in the
INF_FLOW_CONTRACT_APPL_PROPERTY.
|
Modifier and Type | Method and Description |
---|---|
java.util.List<Taclet> |
KeyIO.findTaclets(KeyAst.File ctx) |
java.util.List<Taclet> |
KeyIO.Loader.loadComplete() |
java.util.List<Taclet> |
KeyIO.Loader.loadTaclets() |
Modifier and Type | Method and Description |
---|---|
Taclet |
TacletPBuilder.visitTaclet(KeYParser.TacletContext ctx) |
Modifier and Type | Method and Description |
---|---|
java.util.List<Taclet> |
TacletPBuilder.getTopLevelTaclets() |
ImmutableList<Taclet> |
TacletPBuilder.visitTacletlist(KeYParser.TacletlistContext ctx) |
Constructor and Description |
---|
TacletPBuilder(Services services,
NamespaceSet namespaces,
java.util.HashMap<Taclet,TacletBuilder<? extends Taclet>> taclet2Builder) |
TacletPBuilder(Services services,
NamespaceSet namespaces,
java.util.HashMap<Taclet,TacletBuilder<? extends Taclet>> taclet2Builder) |
Modifier and Type | Method and Description |
---|---|
protected void |
LogicPrinter.printAttribs(Taclet taclet) |
protected void |
LogicPrinter.printDisplayName(Taclet taclet) |
protected void |
LogicPrinter.printFind(Taclet taclet) |
protected void |
LogicPrinter.printGoalTemplates(Taclet taclet) |
protected void |
LogicPrinter.printHeuristics(Taclet taclet) |
void |
LogicPrinter.printTaclet(Taclet taclet)
Pretty-print a taclet.
|
void |
LogicPrinter.printTaclet(Taclet taclet,
SVInstantiations sv,
boolean showWholeTaclet,
boolean declareSchemaVars)
Pretty-print a taclet.
|
protected void |
LogicPrinter.printVarCond(Taclet taclet) |
Modifier and Type | Method and Description |
---|---|
protected void |
LogicPrinter.printRules(ImmutableList<Taclet> rules) |
Modifier and Type | Method and Description |
---|---|
void |
TacletIndex.add(Taclet taclet)
adds a new Taclet with instantiation information to this index.
|
void |
Goal.addTaclet(Taclet rule,
SVInstantiations insts,
boolean isAxiom)
creates a new TacletApp and puts it to the set of TacletApps at the node
of the goal and to the current RuleAppIndex.
|
boolean |
TermTacletAppIndexCacheSet.isRelevantTaclet(Taclet t) |
static boolean |
NodeInfo.isSymbolicExecution(Taclet t) |
Modifier and Type | Method and Description |
---|---|
abstract TacletIndex |
TacletIndexKit.createTacletIndex(java.lang.Iterable<Taclet> tacletSet)
abstract factory method to create a
TacletIndex containing the provided taclets |
static ImmutableSet<NoPosTacletApp> |
TacletIndex.toNoPosTacletApp(java.lang.Iterable<Taclet> rule) |
Modifier and Type | Method and Description |
---|---|
Taclet |
InitConfig.lookupActiveTaclet(Name name) |
Modifier and Type | Method and Description |
---|---|
java.lang.Iterable<Taclet> |
InitConfig.activatedTaclets()
returns the activated taclets of this initial configuration
|
java.util.HashMap<Taclet,TacletBuilder<? extends Taclet>> |
InitConfig.getTaclet2Builder()
Taclet s are constructed using TacletBuilder s this map
contains the pair of a taclet and its builder which is important as
goals of a taclet may depend of the selected choices. |
java.util.HashMap<Taclet,TacletBuilder<? extends Taclet>> |
InitConfig.getTaclet2Builder()
Taclet s are constructed using TacletBuilder s this map
contains the pair of a taclet and its builder which is important as
goals of a taclet may depend of the selected choices. |
ImmutableList<Taclet> |
InitConfig.getTaclets() |
Modifier and Type | Method and Description |
---|---|
void |
InitConfig.addTaclets(java.util.Collection<Taclet> tacs) |
void |
InitConfig.setTaclet2Builder(java.util.HashMap<Taclet,TacletBuilder<? extends Taclet>> taclet2Builder) |
void |
InitConfig.setTaclet2Builder(java.util.HashMap<Taclet,TacletBuilder<? extends Taclet>> taclet2Builder) |
void |
InitConfig.setTaclets(java.util.Collection<Taclet> tacs) |
void |
InitConfig.setTaclets(ImmutableList<Taclet> tacs) |
Modifier and Type | Method and Description |
---|---|
Pair<IObserverFunction,ImmutableSet<Taclet>> |
SpecificationRepository.limitObs(IObserverFunction obs) |
Modifier and Type | Method and Description |
---|---|
protected boolean |
TacletFilterCloseGoal.filter(Taclet taclet) |
boolean |
AnyRuleSetTacletFilter.filter(Taclet taclet) |
protected abstract boolean |
TacletFilter.filter(Taclet taclet) |
protected boolean |
TacletFilterSplitGoal.filter(Taclet taclet) |
boolean |
IHTacletFilter.filter(Taclet taclet) |
Modifier and Type | Class and Description |
---|---|
class |
AntecTaclet
An AntecTaclet represents a taclet whose find part has to match a top level
formula in the antecedent of the sequent.
|
class |
FindTaclet
An abstract class to represent Taclets with a find part.
|
class |
NoFindTaclet
Used to implement a Taclet that has no find part.
|
class |
RewriteTaclet
A RewriteTaclet represents a taclet, whose find can be matched against any
term in the sequent no matter where it occurs.
|
class |
SuccTaclet
A SuccTaclet represents a taclet whose find part has to match a top level
formula in the succedent of the sequent.
|
Modifier and Type | Field and Description |
---|---|
protected TacletExecutor<? extends Taclet> |
Taclet.executor
The taclet executor
|
Modifier and Type | Method and Description |
---|---|
abstract Taclet |
Taclet.setName(java.lang.String s) |
Taclet |
TacletApp.taclet()
returns the taclet the application information is collected for
|
Modifier and Type | Method and Description |
---|---|
TacletExecutor<? extends Taclet> |
Taclet.getExecutor() |
Modifier and Type | Method and Description |
---|---|
protected static boolean |
NoPosTacletApp.checkVarCondNotFreeIn(Taclet taclet,
SVInstantiations instantiations)
checks if the variable conditions of type 'x not free in y' are
hold by the found instantiations.
|
static boolean |
TacletApp.checkVarCondNotFreeIn(Taclet taclet,
SVInstantiations instantiations,
PosInOccurrence pos)
checks if the variable conditions of type 'x not free in y' are hold by
the found instantiations.
|
static NoPosTacletApp |
NoPosTacletApp.createFixedNoPosTacletApp(Taclet taclet,
SVInstantiations instantiations,
Services services)
Create TacletApp with immutable "instantiations", i.e.
|
static NoPosTacletApp |
NoPosTacletApp.createNoPosTacletApp(Taclet taclet)
creates a NoPosTacletApp for the given taclet and no instantiation
information and CHECKS variable conditions as well as it resolves
collisions
|
static NoPosTacletApp |
NoPosTacletApp.createNoPosTacletApp(Taclet taclet,
MatchConditions matchCond,
Services services) |
static NoPosTacletApp |
NoPosTacletApp.createNoPosTacletApp(Taclet taclet,
SVInstantiations instantiations,
ImmutableList<IfFormulaInstantiation> ifInstantiations,
Services services) |
static NoPosTacletApp |
NoPosTacletApp.createNoPosTacletApp(Taclet taclet,
SVInstantiations instantiations,
Services services)
creates a NoPosTacletApp for the given taclet with some known
instantiations and CHECKS variable conditions as well as it
resolves collisions
The ifInstantiations parameter is not
matched against the if sequence, but only stored.
|
protected static boolean |
TacletApp.ifInstsCorrectSize(Taclet p_taclet,
ImmutableList<IfFormulaInstantiation> p_list) |
protected static SVInstantiations |
TacletApp.replaceInstantiation(Taclet taclet,
SVInstantiations insts,
SchemaVariable varSV,
Services services)
returns a new SVInstantiations that modifies the given SVInstantiations
insts at the bound SchemaVariable varSV to a new LogicVariable.
|
protected static SVInstantiations |
TacletApp.resolveCollisionVarSV(Taclet taclet,
SVInstantiations insts,
Services services)
resolves collisions between bound SchemaVariables in an SVInstantiation
|
void |
TacletSchemaVariableCollector.visit(Taclet taclet,
boolean visitAddrules)
collects all schema variables of a taclet
|
void |
SVNameCorrespondenceCollector.visit(Taclet taclet,
boolean visitAddrules)
collects all correspondences in a taclet
|
protected void |
TacletSchemaVariableCollector.visitFindPart(Taclet taclet) |
protected void |
TacletSchemaVariableCollector.visitGoalTemplates(Taclet taclet,
boolean visitAddrules) |
void |
TacletSchemaVariableCollector.visitWithoutAddrule(Taclet taclet)
collects all variables in a Taclet but ignores the variables that appear
only in the addrule sections of the Taclet
|
Constructor and Description |
---|
InfFlowValidityData(Term preAssumption,
Term postAssumption,
Taclet taclet) |
NoPosTacletApp(Taclet taclet)
creates a NoPosTacletApp for the given taclet and no instantiation
information
|
Modifier and Type | Class and Description |
---|---|
class |
TacletExecutor<TacletKind extends Taclet>
Encapsulates the application engine of taclets.
|
Modifier and Type | Field and Description |
---|---|
protected TacletKind |
TacletExecutor.taclet |
Modifier and Type | Method and Description |
---|---|
protected void |
TacletExecutor.applyAddrule(ImmutableList<Taclet> rules,
Goal goal,
Services services,
MatchConditions matchCond)
adds the given rules (i.e.
|
Modifier and Type | Method and Description |
---|---|
Taclet |
TacletInstantiations.taclet() |
Constructor and Description |
---|
TacletInstantiations(Taclet rule,
ImmutableMap<SchemaVariable,Term> instantiations) |
Modifier and Type | Method and Description |
---|---|
abstract TacletMatcher |
TacletMatcherKit.createTacletMatcher(Taclet taclet)
the creator method returning the matcher for the specified taclet
|
Constructor and Description |
---|
LegacyTacletMatcher(Taclet taclet) |
Constructor and Description |
---|
VMTacletMatcher(Taclet taclet) |
Modifier and Type | Class and Description |
---|---|
class |
TacletBuilder<T extends Taclet>
abstract taclet builder class to be inherited from taclet builders
specialised for their concrete taclet variant
|
Modifier and Type | Field and Description |
---|---|
protected Taclet |
TacletBuilder.taclet |
Modifier and Type | Method and Description |
---|---|
Taclet |
TacletGenerator.generateAxiomTaclet(Name tacletName,
Term originalAxiom,
ImmutableList<ProgramVariable> programVars,
KeYJavaType kjt,
RuleSet ruleSet,
TermServices services)
Returns a no-find taclet to the passed axiom.
|
Taclet |
TacletGenerator.generateRelationalRepresentsTaclet(Name tacletName,
Term originalAxiom,
KeYJavaType kjt,
IObserverFunction target,
java.util.List<? extends ProgramVariable> heaps,
ProgramVariable self,
ImmutableList<ProgramVariable> paramVars,
java.util.Map<LocationVariable,ProgramVariable> atPreVars,
boolean satisfiabilityGuard,
TermServices services) |
Taclet |
TacletGenerator.generateRewriteTaclet(Name tacletName,
Term originalFind,
Term originalAxiom,
ImmutableList<ProgramVariable> programVars,
RuleSet ruleSet,
TermServices services) |
Modifier and Type | Method and Description |
---|---|
ImmutableSet<Taclet> |
TacletGenerator.generateContractAxiomTaclets(Name name,
Term originalPre,
Term originalPost,
Term originalMby,
KeYJavaType kjt,
IObserverFunction target,
java.util.List<? extends ProgramVariable> heaps,
ProgramVariable originalSelfVar,
ProgramVariable originalResultVar,
java.util.Map<LocationVariable,ProgramVariable> atPreVars,
ImmutableList<ProgramVariable> originalParamVars,
ImmutableSet<Pair<Sort,IObserverFunction>> toLimit,
boolean satisfiabilityGuard,
TermServices services) |
ImmutableSet<Taclet> |
TacletGenerator.generateFunctionalRepresentsTaclets(Name name,
Term originalPreTerm,
Term originalRepresentsTerm,
KeYJavaType kjt,
IObserverFunction target,
java.util.List<? extends ProgramVariable> heaps,
ProgramVariable self,
ImmutableList<ProgramVariable> paramVars,
java.util.Map<LocationVariable,ProgramVariable> atPreVars,
ImmutableSet<Pair<Sort,IObserverFunction>> toLimit,
boolean satisfiability,
Services services) |
ImmutableSet<Taclet> |
TacletGenerator.generatePartialInvTaclet(Name name,
java.util.List<SchemaVariable> heapSVs,
SchemaVariable selfSV,
SchemaVariable eqSV,
Term term,
KeYJavaType kjt,
ImmutableSet<Pair<Sort,IObserverFunction>> toLimit,
boolean isStatic,
boolean eqVersion,
Services services) |
ImmutableList<Taclet> |
TacletGoalTemplate.rules()
the goal of a Taclet may introduce new rules.
|
Constructor and Description |
---|
AntecSuccTacletGoalTemplate(Sequent addedSeq,
ImmutableList<Taclet> addedRules,
Sequent replacewith) |
AntecSuccTacletGoalTemplate(Sequent addedSeq,
ImmutableList<Taclet> addedRules,
Sequent replacewith,
ImmutableSet<SchemaVariable> pvs)
creates new Goaldescription
|
RewriteTacletGoalTemplate(Sequent addedSeq,
ImmutableList<Taclet> addedRules,
Term replacewith) |
RewriteTacletGoalTemplate(Sequent addedSeq,
ImmutableList<Taclet> addedRules,
Term replacewith,
ImmutableSet<SchemaVariable> pvs)
creates new Goaldescription
|
TacletGoalTemplate(Sequent addedSeq,
ImmutableList<Taclet> addedRules)
creates new Goaldescription
same effect as
new TacletGoalTemplate(addedSeq,
addedRules,
SetAsListOf. |
TacletGoalTemplate(Sequent addedSeq,
ImmutableList<Taclet> addedRules,
ImmutableSet<SchemaVariable> addedProgVars)
creates new Goaldescription
|
TacletPrefixBuilder(TacletBuilder<? extends Taclet> tacletBuilder) |
Modifier and Type | Method and Description |
---|---|
java.util.Collection<Taclet> |
SMTSettings.getTaclets() |
Modifier and Type | Method and Description |
---|---|
java.util.Collection<Taclet> |
SMTSettings.getTaclets()
The set of taclets that should be used.
|
Modifier and Type | Method and Description |
---|---|
Term |
SMTTacletTranslator.translate(Taclet taclet) |
Modifier and Type | Method and Description |
---|---|
abstract ImmutableSet<Taclet> |
ClassAxiom.getTaclets(ImmutableSet<Pair<Sort,IObserverFunction>> toLimit,
Services services)
The axiom as one or many taclets, where the non-defining occurrences of
the passed observers are replaced by their "limited" counterparts.
|
ImmutableSet<Taclet> |
ClassAxiomImpl.getTaclets(ImmutableSet<Pair<Sort,IObserverFunction>> toLimit,
Services services) |
ImmutableSet<Taclet> |
QueryAxiom.getTaclets(ImmutableSet<Pair<Sort,IObserverFunction>> toLimit,
Services services) |
ImmutableSet<Taclet> |
PartialInvAxiom.getTaclets(ImmutableSet<Pair<Sort,IObserverFunction>> toLimit,
Services services) |
ImmutableSet<Taclet> |
ContractAxiom.getTaclets(ImmutableSet<Pair<Sort,IObserverFunction>> toLimit,
Services services) |
ImmutableSet<Taclet> |
RepresentsAxiom.getTaclets(ImmutableSet<Pair<Sort,IObserverFunction>> toLimit,
Services services) |
ImmutableSet<Taclet> |
ModelMethodExecution.getTaclets(ImmutableSet<Pair<Sort,IObserverFunction>> toLimit,
Services services) |
Modifier and Type | Method and Description |
---|---|
protected static boolean |
TruthValueTracingUtil.isClosingRule(Taclet taclet)
Checks if the
Taclet is a closing rule. |
Modifier and Type | Method and Description |
---|---|
Taclet |
TacletFormula.getTaclet() |
Modifier and Type | Method and Description |
---|---|
Term |
SkeletonGenerator.translate(Taclet t,
TermServices services)
Override this method to introduce a translating mechanism for taclets.
|
Term |
DefaultTacletTranslator.translate(Taclet taclet,
TermServices services)
Translates a RewriteTaclet to a formula.
|
java.lang.String |
TacletVisitor.visit(Taclet taclet) |
java.lang.String |
TacletVisitor.visit(Taclet taclet,
boolean visitAddrules) |
protected void |
TacletVisitor.visitFindPart(Taclet taclet) |
protected void |
TacletVisitor.visitGoalTemplates(Taclet taclet,
boolean visitAddrules) |
Modifier and Type | Method and Description |
---|---|
Taclet |
AssumptionFormula.getTaclet() |
Modifier and Type | Method and Description |
---|---|
boolean |
DefaultTacletSetTranslation.eventInstantiationFailure(GenericSort dest,
Sort sort,
Taclet t,
Term term) |
boolean |
TranslationListener.eventInstantiationFailure(GenericSort dest,
Sort sort,
Taclet t,
Term term)
Called when the translator can not instantiate a generic sort
with a particular sort in the given term.
|
TacletFormula |
AssumptionGenerator.translate(Taclet t,
ImmutableSet<Sort> sorts,
int maxGeneric) |
Modifier and Type | Method and Description |
---|---|
java.util.Collection<java.lang.String> |
SupportedTaclets.getMissingTaclets(java.util.Collection<Taclet> taclets) |
Constructor and Description |
---|
AssumptionFormula(Taclet taclet,
java.util.Collection<Term> formula,
java.lang.String status) |
AssumptionFormula(Taclet taclet,
java.util.Collection<Term> formula,
java.lang.String status,
de.uka.ilkd.key.taclettranslation.assumptions.TacletConditions conditions) |
Modifier and Type | Method and Description |
---|---|
Taclet |
TacletSoundnessPOLoader.TacletInfo.getTaclet() |
Modifier and Type | Method and Description |
---|---|
ImmutableSet<Taclet> |
TacletSoundnessPOLoader.TacletFilter.filter(java.util.List<TacletSoundnessPOLoader.TacletInfo> taclets) |
ImmutableSet<Taclet> |
TacletSoundnessPOLoader.getResultingTaclets() |
ImmutableSet<Taclet> |
TacletSoundnessPOLoader.getResultingTacletsForOriginalProof() |
abstract ImmutableSet<Taclet> |
TacletLoader.getTacletsAlreadyInUse()
get the taclet base which is considered fix (?)
|
ImmutableSet<Taclet> |
TacletLoader.TacletFromFileLoader.getTacletsAlreadyInUse() |
ImmutableSet<Taclet> |
TacletLoader.KeYsTacletsLoader.getTacletsAlreadyInUse() |
abstract ImmutableSet<Taclet> |
TacletLoader.loadAxioms()
get the set of axioms from the axiom files if applicable.
|
ImmutableSet<Taclet> |
TacletLoader.TacletFromFileLoader.loadAxioms() |
ImmutableSet<Taclet> |
TacletLoader.KeYsTacletsLoader.loadAxioms() |
abstract ImmutableList<Taclet> |
TacletLoader.loadTaclets()
get the set of taclets to examine
(either from the system or from a file)
|
ImmutableList<Taclet> |
TacletLoader.TacletFromFileLoader.loadTaclets() |
ImmutableList<Taclet> |
TacletLoader.KeYsTacletsLoader.loadTaclets() |
Modifier and Type | Method and Description |
---|---|
void |
TacletLoader.manageAvailableTaclets(InitConfig initConfig,
Taclet tacletToProve)
When proving existing system taclets, all rules which occurred prior to
the desired taclet need to be elminated from the set of available taclets
to avoid circular proofs.
|
TacletFormula |
LemmaGenerator.translate(Taclet taclet,
TermServices services) |
Modifier and Type | Method and Description |
---|---|
ProofAggregate |
ProofObligationCreator.create(ImmutableSet<Taclet> taclets,
InitConfig[] initConfigs,
ImmutableSet<Taclet> axioms,
java.util.Collection<TacletSoundnessPOLoader.LoaderListener> listeners)
Creates for each taclet in
taclets a proof obligation
containing the corresponding FOL formula of the taclet. |
ProofAggregate |
ProofObligationCreator.create(ImmutableSet<Taclet> taclets,
InitConfig[] initConfigs,
ImmutableSet<Taclet> axioms,
java.util.Collection<TacletSoundnessPOLoader.LoaderListener> listeners)
Creates for each taclet in
taclets a proof obligation
containing the corresponding FOL formula of the taclet. |
void |
TacletSoundnessPOLoader.LoaderListener.stopped(ProofAggregate p,
ImmutableSet<Taclet> taclets,
boolean addAsAxioms) |
Constructor and Description |
---|
TacletInfo(Taclet taclet,
boolean alreadyInUse,
boolean notSupported) |
Constructor and Description |
---|
UserDefinedSymbols(NamespaceSet referenceNamespaces,
ImmutableSet<Taclet> axioms) |
Modifier and Type | Method and Description |
---|---|
boolean |
MediatorProofControl.selectedTaclet(Taclet taclet,
Goal goal,
PosInOccurrence pos) |
Modifier and Type | Method and Description |
---|---|
Taclet |
ProofExplorationService.getCutTaclet()
Finds the `cut` taclet in the current proof environment.
|
Copyright © 2003-2019 The KeY-Project.