Skip to content

Version 0.7
Compare
Choose a tag to compare
@dominique-unruh dominique-unruh released this 15 Aug 21:38
· 133 commits to master since this release
v0.7
6aedcf1

Installation instructions

See https://dominique-unruh.github.io/qrhl-tool/install.html

Changes

  • Caching computations (redoing already done proof steps is fast)
  • Auto-reloading changed included and .thy files
  • Support for Isabelle 2021-1
  • Focusing commands { } + etc.
  • Syntax highlighting in ProofGeneral
  • New command isabelle_cmd for arbitrary Isabelle toplevel commands
  • equal tactic now gives very detailed explanation of its reasoning (for understanding failures)
  • Config file .qrhl-tool.conf also found in home directory
  • isabelle command allows to configure Isabelle session
  • Isabelle session configured in current directory detected (ROOT/ROOTS file)
  • Many bugfixes
  • Improved background theory in Isabelle (more proofs, session Bounded_Operators fully proven)
Assets 3
Loading