# Macros
Generated on: Sat Sep 09 23:02:00 CEST 2017 by `gendoc.groovy`.
Covering the macros of [KeY](http://key-project.org).
## Full Information Flow Auto Pilot (`infflow-autopilot`)
Information Flow
- Search exhaustively for applicable position, then
- Start auxiliary computation
- Finish symbolic execution
- Try to close as many goals as possible
- Apply macro recursively
- Finish auxiliary computation
- Use information flow contracts
- Try to close as many goals as possible

## Close provable goals below (`tryclose`)
null
Closes closable goals, leave rest untouched (see settings AutoPrune). Applies only to goals beneath the selected node.
## Update Simplification Only (`simp-upd`)
Simplification
Applies only update simplification rules
## Full Auto Pilot (`autopilot`)
Auto Pilot
- Finish symbolic execution
- Separate proof obligations
- Expand invariant definitions
- Try to close all proof obligations

## Finish symbolic execution (`symbex`)
Auto Pilot
Continue automatic strategy application until no more modality is on the sequent.
## Propositional expansion (w/ splits) (`split-prop`)
Propositional
Apply rules to decompose propositional toplevel formulas; splits the goal if necessary
## Heap Simplification (`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.
## Auto pilot (preparation only) (`autopilot-prep`)
Auto Pilot
- Finish symbolic execution
- Separate proof obligations
- Expand invariant definitions

## Propositional expansion (w/o splits) (`nosplit-prop`)
Propositional
Apply rules to decompose propositional toplevel formulas; does not split the goal.
## One Single Proof Step (`onestep`)
Simplification
One single proof step is applied