Version 4.4

KeYmaera X version 4.4

• [Core] New: N-ary formula and function definitions.
  For example,
  define a binary function 'sum' as: sum(R,R) = ( ._0 + ._1).
  define predicate 'sumgt' as: sumgt(R,R,R) <-> ( sum(._0,._1) > ._2 ).
• [Parser] New: Program definitions.
  For example, HP increment ::= { x:=x+1; }.
• [Tactics] New: use finished proofs as lemmas, for example useLemma({Name of proved model}) when the open goal matches the lemma literally, useLemma({Name of proved model}, {prop}) to apply the lemma with propositional reasoning.
• [Tools] New: proof statistics after checking archives with -check
• [Tools] New: C control code synthesis (feature preview)
• [Tools] Improved: C monitor code synthesis (feature preview)
• Stability improvements: archive checking, ODE solution ordering