--- a/NEWS Wed Sep 22 12:41:40 2021 +0200
+++ b/NEWS Wed Sep 22 14:32:20 2021 +0200
@@ -20,7 +20,7 @@
in interactive mode, but it could occasionally cause unnecessary
slowdown. It can be disabled like this:
- context notes [[show_results = true]]
+ context notes [[show_results = false]]
begin
definition "test = True"
theorem test by (simp add: test_def)
@@ -137,7 +137,7 @@
* 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".
+"no_lattice_syntax". Minor INCOMPATIBILITY.
* Theory "HOL-Library.Multiset": dedicated predicate "multiset" is gone,
use explict expression instead. Minor INCOMPATIBILITY.