# HG changeset patch
# User wenzelm
# Date 1730026112 -3600
# Node ID ccd8e404d7d9297a5b716b11d8552def4f5c49f1
# Parent  fb391ad09b3cf01dd58713534b094e77bab43d6f
clarified section structure;

diff -r fb391ad09b3c -r ccd8e404d7d9 NEWS
--- a/NEWS	Sun Oct 27 11:46:04 2024 +0100
+++ b/NEWS	Sun Oct 27 11:48:32 2024 +0100
@@ -9,18 +9,17 @@
 
 *** General ***
 
-* Command "unbundle b" and its variants like "context includes b" allow
-an optional name prefix with the reserved word "no": "unbundle no b"
-etc. This inverts the polarity of bundled declarations like 'notation'
-vs. 'no_notation', and thus avoids redundant bundle definitions like
-"foobar_syntax" vs. "no_foobar_syntax", because "no foobar_syntax" may
-be used instead. Consequently, the syntax for multiple bundle names has
-been changed slightly, demanding an explicit 'and' keyword. Minor
-INCOMPATIBILITY.
-
-* Command "open_bundle b" is like "bundle b" followed by "unbundle b",
-so its declarations are applied immediately, but also named for later
-re-use: "unbundle no b" etc.
+* The Simplifier now supports special "congprocs", using keyword
+'congproc' or 'weak_congproc' in the 'simproc_setup' command (or ML
+antiquotation of the same name). See also
+~~/src/HOL/Imperative_HOL/ex/Congproc_Ex.thy for further explanations
+and examples.
+
+* The attribute "cong_format" produces the internal format of Simplifier
+"cong" rules, notably for congproc implementations.
+
+
+*** Inner syntax --- the term language ***
 
 * Blocks for pretty-printing (of types, terms, props etc.) now support
 properties "open_block" (bool) and "notation" (string as cartouche).
@@ -63,14 +62,45 @@
 AST rewriting (command 'translations'). Rare INCOMPATIBILITY, slightly
 different results could be printed (often slightly "better" ones).
 
-* The Simplifier now supports special "congprocs", using keyword
-'congproc' or 'weak_congproc' in the 'simproc_setup' command (or ML
-antiquotation of the same name). See also
-~~/src/HOL/Imperative_HOL/ex/Congproc_Ex.thy for further explanations
-and examples.
-
-* The attribute "cong_format" produces the internal format of Simplifier
-"cong" rules, notably for congproc implementations.
+* Command "unbundle b" and its variants like "context includes b" allow
+an optional name prefix with the reserved word "no": "unbundle no b"
+etc. This inverts the polarity of bundled declarations like 'notation'
+vs. 'no_notation', and thus avoids redundant bundle definitions like
+"foobar_syntax" vs. "no_foobar_syntax", because "no foobar_syntax" may
+be used instead. Consequently, the syntax for multiple bundle names has
+been changed slightly, demanding an explicit 'and' keyword. Minor
+INCOMPATIBILITY.
+
+* Command "open_bundle b" is like "bundle b" followed by "unbundle b",
+so its declarations are applied immediately, but also named for later
+re-use: "unbundle no b" etc.
+
+* Various HOL declaration bundles support adhoc modification of
+notation, notably like this:
+
+  unbundle no list_syntax
+  unbundle no list_enumeration_syntax
+  unbundle no list_comprehension_syntax
+  unbundle no relcomp_syntax
+  unbundle no converse_syntax
+  unbundle no rtrancl_syntax
+  unbundle no trancl_syntax
+  unbundle no reflcl_syntax
+  unbundle no abs_syntax
+  unbundle no floor_ceiling_syntax
+  unbundle no uminus_syntax
+  unbundle no funcset_syntax
+
+This is more robust than individual 'no_syntax' / 'no_notation'
+commands, which need to copy mixfix declarations from elsewhere and thus
+break after changes in the library.
+
+* Theory "HOL-Library.Datatype_Records" provides bundle
+"datatype_record_syntax" to exchange its alternative notation versus
+regular "record_syntax". This also allows to swap record syntax later
+on, notably like this:
+
+  unbundle no datatype_record_syntax
 
 
 *** Isabelle/VSCode Prover IDE ***
@@ -105,33 +135,6 @@
     This outputs a suggestion with instantiations of the facts using the
     "of" attribute (e.g. "assms(1)[of x]").
 
-* Various declaration bundles support adhoc modification of notation,
-notably like this:
-
-  unbundle no list_syntax
-  unbundle no list_enumeration_syntax
-  unbundle no list_comprehension_syntax
-  unbundle no relcomp_syntax
-  unbundle no converse_syntax
-  unbundle no rtrancl_syntax
-  unbundle no trancl_syntax
-  unbundle no reflcl_syntax
-  unbundle no abs_syntax
-  unbundle no floor_ceiling_syntax
-  unbundle no uminus_syntax
-  unbundle no funcset_syntax
-
-This is more robust than individual 'no_syntax' / 'no_notation'
-commands, which need to copy mixfix declarations from elsewhere and thus
-break after changes in the library.
-
-* Theory "HOL-Library.Datatype_Records" provides bundle
-"datatype_record_syntax" to exchange its alternative notation versus
-regular "record_syntax". This also allows to swap record syntax later
-on, notably like this:
-
-  unbundle no datatype_record_syntax
-
 * Theory "HOL.Wellfounded":
   - Removed lemma wellorder.wfP_less. Use wellorder.wfp_on_less instead.
     Minor INCOMPATIBILITY.
@@ -181,6 +184,8 @@
 
 *** ML ***
 
+* Antiquotation \<^bundle>\<open>name\<close> inlines a formally checked bundle name.
+
 * The new operation Pattern.rewrite_term_yoyo alternates top-down,
 bottom-up, top-down etc. until a normal form is reached. This often
 works better than former rewrite_term_top --- that is still available,
@@ -208,8 +213,6 @@
 Note that basic Markup.markup cannot be used for Latex output: proper
 Pretty.T operations are required (e.g. Pretty.mark_str).
 
-* Antiquotation \<^bundle>\<open>name\<close> inlines a formally checked bundle name.
-
 
 *** System ***