*** HOL ***
* An updated version of the veriT solver is now included as Isabelle
component. It can be used in the "smt" proof method via "smt (verit)" or
via "declare [[smt_solver = verit]]" in the context; see also session
HOL-Word-SMT_Examples.
*** System ***
* Update/rebuild external provers on currently supported OS platforms,
notably E prover 2.5, SPASS 3.8ds, CSDP 6.1.1.
This refers to various changes in the past few weeks, culminating in current
Isabelle/b5f7fc7d2323.
We still have until approx. 15-Dec-2020 to include/update more external
provers. Due to some new "isabelle build_XYZ" tools this is getting more and
more robust and reproducibly, on an increasing number of platforms:
arm64-linux already works for many things (even though it is strictly speaking
a toy right now).
Makarius
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
