Version 4.9.0

Version 4.9.0 provides a restructured tactic framework and module separation. Model organization, shortcut notation in user definitions, more transparent proof rule display, and improved support for starting and checking lemmas.

• [UI] More transparent display of proof rules with and without context
• [UI] Differential invariant (dI) proofs can be constructed interactively in the UI with dIrule. Automatic completion is available as dIclose
• [UI] Organize models into folders with hierarchical archive entry names
• [UI] Prove lemmas used in a theorem when opening the theorem, start new lemmas from open proof subgoals
• [Tactic] Framework restructuring, Scala annotation macros @Axiom for derived axiom registration, @Tactic for tactic registration, tactic presentation, and tactic documentation
• [Tactic] Step-by-step replay: expand definitions, use lemmas
• [Tactic] Framework extensions and robustness: polynomial arithmetic, differential equation proving, Taylor models, sum-of-squares solving
• [Backend] Basic heuristic for time-triggered systems in Pegasus invariant generator
• [Backend] Update Z3 4.8.9
• [Parser] Shortcut notation for unary function symbols, system constants, unary predicates and predicationals; uniform across definitions, models, annotations, and tactics
• [Parser] ASCII game symbol for demonic choice -- synonymous with ∩
• [Core] Compilable standalone to keymaerax-core.jar