merged
authordesharna
Wed, 22 Sep 2021 14:32:20 +0200
changeset 74708 783382bbd2b9
parent 74704 fb8ce6090437 (current diff)
parent 74707 4974c3697fee (diff)
child 74709 4f5e67b247e1
merged
--- 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.