# HG changeset patch
# User desharna
# Date 1633595688 -7200
# Node ID 253c98aa935a4f0432e63f0fec692ccb0fd271ab
# Parent  f4a80cfb27819d22ea873481bf1608de649bed5f
NEWS and CONTRIBUTORS

diff -r f4a80cfb2781 -r 253c98aa935a CONTRIBUTORS
--- 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.
 
diff -r f4a80cfb2781 -r 253c98aa935a NEWS
--- 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