--- a/CONTRIBUTORS Thu Oct 07 10:20:10 2021 +0200
+++ b/CONTRIBUTORS Thu Oct 07 10:34:48 2021 +0200
@@ -6,15 +6,19 @@
Contributions to Isabelle2021-1
-------------------------------
+* September .. October 2021: Jasmin Blanchette, Martin Desharnais,
+ Mathias Fleury, Makarius Wenzel
+ Upgrade of automatic theorem provers in Sledgehammer and the smt tactic.
+
* July .. September 2021: Makarius Wenzel
Significantly improved Isabelle/Haskell library.
+* July .. September 2021: Jasmin Blanchette, Martin Desharnais
+ Various improvements to Sledgehammer.
+
* July 2021: Florian Haftmann
Further consolidation of bit operations and word types.
-* July 2021: Jasmin Blanchette and Martin Desharnais
- Various improvements to Sledgehammer.
-
* June 2021: Florian Haftmann
More context situations susceptible to global_interpretation.
--- a/NEWS Thu Oct 07 10:20:10 2021 +0200
+++ b/NEWS Thu Oct 07 10:34:48 2021 +0200
@@ -197,6 +197,7 @@
Zipperposition 2.1
- Adjusted default provers:
cvc4 vampire verit e spass z3 zipperposition
+ - Adjusted Zipperposition's slicing.
- Removed legacy "lam_lifting" (synonym for "lifting") from option
"lam_trans". Minor INCOMPATIBILITY.
- Renamed "hide_lams" to "opaque_lifting" in option "lam_trans". Minor
@@ -205,8 +206,11 @@
rewritten using combinators, but the combinators are kept opaque,
i.e. without definitions.
-* Metis: Renamed option "hide_lams" to "opaque_lifting". Minor
-INCOMPATIBILITY.
+* Metis:
+ - Renamed option "hide_lams" to "opaque_lifting". Minor INCOMPATIBILITY.
+ - Updated the Metis prover underlying the "metis" proof method to
+ version 2.4 (release 20200713). The new version fixes one
+ implementation defect. Very slight INCOMPATIBILITY.
* Theory HOL-Library.Lattice_Syntax has been superseded by bundle
"lattice_syntax": it can be used in a local context via 'include' or in