Generated on: ${new Date()} by gendoc.groovy
.
Covering the macros of KeY.
autopilot
)¶Auto Pilot
autopilot-prep
)¶Auto Pilot
infflow-autopilot
)¶Information Flow
nosplit-prop
)¶Propositional
Apply rules to decompose propositional toplevel formulas; does not split the goal.
onestep
)¶Simplification
One single proof step is applied
simp-heap
)¶Simplification
This macro performs simplification of Heap and LocSet terms. It applies simplification rules (including the “unoptimized” select rules), One Step Simplification, alpha, and delta rules.
simp-upd
)¶Simplification
Applies only update simplification rules
split-prop
)¶Propositional
Apply rules to decompose propositional toplevel formulas; splits the goal if necessary
symbex
)¶Auto Pilot
Continue automatic strategy application until no more modality is on the sequent.
tryclose
)¶null
Closes closable goals, leave rest untouched (see settings AutoPrune). Applies only to goals beneath the selected node.