NEWS

 min.absorb4, max.absorb1, max.absorb2, max.absorb3, max.absorb4. Minor
 INCOMPATIBILITY.
 
 * Sledgehammer:
   - Update of bundled provers:
-      E 2.6
-      Vampire 4.6 (with Open Source license)
-      veriT 2021.06-rmx
-      Zipperposition 2.1
+      . E 2.6
+      . Vampire 4.6 (with Open Source license)
+      . veriT 2021.06.1-rmx
+      . Zipperposition 2.1
+      . Z3 4.4.1 for arm64-linux, which approximates Z3 4.4.0pre,
+        but sometimes failes or crashes
   - 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.

   - 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.
 
 * Nitpick: External solver "MiniSat" is available for all supported
-Isabelle platforms (including Windows and ARM); while "MiniSat_JNI" only
-works for Intel Linux and macOS.
+Isabelle platforms (including 64bit Windows and ARM); while
+"MiniSat_JNI" only works for Intel Linux and macOS.
 
 * Theory HOL-Library.Lattice_Syntax has been superseded by bundle
 "lattice_syntax": it can be used in a local context via 'include' or in
 a global theory via 'unbundle'. The opposite declarations are bundled as
 "no_lattice_syntax". Minor INCOMPATIBILITY.

 development: libphutil has been discontinued. Minor INCOMPATIBILITY:
 existing server installations should remove libphutil from
 /usr/local/bin/isabelle-phabricator-upgrade and each installation root
 directory (e.g. /var/www/phabricator-vcs/libphutil).
 
-* Experimental support for arm64-linux platform. The reference platform
-is Raspberry Pi 4 with 8 GB RAM running Pi OS (64 bit).
+* Almost complete support for arm64-linux platform. The reference
+platform is Raspberry Pi 4 with 8 GB RAM running Pi OS (64 bit).
 
 * Support for Apple Silicon, using mostly x86_64-darwin runtime
 translation via Rosetta 2 (e.g. Poly/ML and external provers), but also
 some native arm64-darwin executables (e.g. Java).