# HG changeset patch
# User wenzelm
# Date 1637928435 -3600
# Node ID 743b114bdb419293e57579a43c67705a71e7c05c
# Parent  8fe987615ffec9cce7da5bbf4af0fdff0c0fa83b
NEWS on "isabelle mirabelle";

diff -r 8fe987615ffe -r 743b114bdb41 NEWS
--- a/NEWS	Fri Nov 26 13:05:36 2021 +0100
+++ b/NEWS	Fri Nov 26 13:07:15 2021 +0100
@@ -208,6 +208,11 @@
 min.absorb4, max.absorb1, max.absorb2, max.absorb3, max.absorb4. Minor
 INCOMPATIBILITY.
 
+* The Mirabelle testing tool is now part of Main HOL, and accessible via
+the command-line tool "isabelle mirabelle" (implemented in
+Isabelle/Scala). It has become more robust and supports parallelism
+within Isabelle/ML.
+
 * Nitpick: External solver "MiniSat" is available for all supported
 Isabelle platforms (including 64bit Windows and ARM); while
 "MiniSat_JNI" only works for Intel Linux and macOS.