Skip to content

Version 4.9.4

Compare
Choose a tag to compare
@smitsch smitsch released this 17 Jun 10:13
· 1806 commits to master since this release
4.9.4

Version 4.9.4 provides an improved definitions UI to supply proof parameters and modeling assumptions,
more robust tactic recording with formula search locators everywhere, tactic branch labels,
as well as backend tool and parser updates.

  • UI: tactic syntax highlighting, executing custom tactics from tactic editor with alt-click (atomic) or shift-click (step-by-step)
  • Tactics: positive-mention "using", e.g. QE using "x>0 :: x>=0 :: nil"
  • Tactics: formula search locators when recording tactics
  • Tactics: search locator notation #...# to identify sub-positions, e.g., dI('R=="x>=0 -> #[{x'=1}]x>=0#")
  • Tactics: branch labels and case matching,
    e.g., loop("J", 'R=="[{a;}*]S") <( "Init": r, "Use": s, "Step": t ) to execute tactic r on branch "Init" etc.
    e.g., andR('R=="x>=0 & y<=2") <( "x>=0": s, "y<=2": t ) to execute tactic s on branch "x>=0" etc.
  • Tactics: better support for differential symbols in quantifiers
  • Tactics: improved ODE support for stability proofs
  • Backend: support for Mathematica 12.2 and 12.3 (MacOS)