NEWS
changeset 72971 162b71f7e554
parent 72969 5bc7fd5379ef
child 72972 31ff3c962937
--- a/NEWS	Mon Dec 21 13:03:23 2020 +0100
+++ b/NEWS	Mon Dec 21 13:58:11 2020 +0100
@@ -110,6 +110,9 @@
 via "declare [[smt_solver = verit]]" in the context; see also session
 HOL-Word-SMT_Examples.
 
+* Zipperposition 2.0 is included as Isabelle component for
+experimentation, e.g. in "sledgehammer [prover = zipperposition]".
+
 * Nitpick/Kodkod may be invoked directly within the running
 Isabelle/Scala session (instead of an external Java process): this
 improves reactivity and saves resources. This experimental feature is
@@ -246,9 +249,6 @@
 * Update/rebuild external provers on currently supported OS platforms,
 notably CVC4 1.8, E prover 2.5, SPASS 3.8ds, CSDP 6.1.1.
 
-* External prover Zipperposition 2.0 is available as component for
-experimentation.
-
 * Discontinued obsolete isabelle display tool, and DVI_VIEWER settings
 variable.