# HG changeset patch
# User wenzelm
# Date 1632176455 -7200
# Node ID eb54c0604ca5d699c00beecde5099e1dff3b2550
# Parent  ead56ad40e15b626186ce83a455860597d0ea414
NEWS;

diff -r ead56ad40e15 -r eb54c0604ca5 NEWS
--- a/NEWS	Tue Sep 21 00:20:47 2021 +0200
+++ b/NEWS	Tue Sep 21 00:20:55 2021 +0200
@@ -9,6 +9,12 @@
 
 *** General ***
 
+* Commands 'syntax' and 'no_syntax' now work in a local theory context,
+but there is no proper way to refer to local entities --- in contrast to
+'notation' and 'no_notation'. Local syntax works well with 'bundle',
+e.g. see "lattice_syntax" vs. "no_lattice_syntax" in theory Main of
+Isabelle/HOL.
+
 * Configuration option "show_results" controls output of final results
 in commands like 'definition' or 'theorem'. Output is normally enabled
 in interactive mode, but it could occasionally cause unnecessary
@@ -128,6 +134,11 @@
 
 *** HOL ***
 
+* 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".
+
 * Theory "HOL-Library.Multiset": dedicated predicate "multiset" is gone,
 use explict expression instead. Minor INCOMPATIBILITY.