--- a/NEWS Sat Sep 25 07:45:27 2021 +0000
+++ b/NEWS Sun Sep 26 20:13:28 2021 +0200
@@ -44,6 +44,15 @@
Isabelle/jEdit.
+*** Isar ***
+
+* The improper proof command 'guess' is no longer part of by Pure, but
+provided by the separate theory "Pure-ex.Guess". INCOMPATIBILITY,
+existing applications need to import session "Pure-ex" and theory
+"Pure-ex.Guess". Afterwards it is usually better eliminate the 'guess'
+command, using explicit 'obtain' instead.
+
+
*** Isabelle/jEdit Prover IDE ***
* More robust 'proof' outline for method "induct": support nested cases.