# 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
  1. Search exhaustively for applicable position, then
  2. Start auxiliary computation
  3. Finish symbolic execution
  4. Try to close as many goals as possible
  5. Apply macro recursively
  6. Finish auxiliary computation
  7. Use information flow contracts
  8. 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
  1. Finish symbolic execution
  2. Separate proof obligations
  3. Expand invariant definitions
  4. 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
  1. Finish symbolic execution
  2. Separate proof obligations
  3. 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