# HG changeset patch
# User wenzelm
# Date 1727953291 -7200
# Node ID 92768949a9234945bc1c5f54158df5011bbe67e0
# Parent  28ef01901650e95601ae2124cb43054ecc3d460a# Parent  ad5fc948e053b866f9dbf62cefb7a2ed0689cb0a
merged

diff -r 28ef01901650 -r 92768949a923 NEWS
--- a/NEWS	Wed Oct 02 18:32:36 2024 +0200
+++ b/NEWS	Thu Oct 03 13:01:31 2024 +0200
@@ -9,6 +9,10 @@
 
 *** General ***
 
+* 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.
+
 * Inner syntax translations now support formal dependencies via commands
 'syntax_types' or 'syntax_consts'. This is essentially an abstract
 specification of the effect of 'translations' (or translation functions
@@ -43,6 +47,19 @@
 
 *** HOL ***
 
+* Various declaration bundles support adhoc modification of notation,
+notably like this:
+
+  unbundle no_list_syntax
+  unbundle no_listcompr_syntax
+  unbundle no_rtrancl_syntax
+  unbundle no_trancl_syntax
+  unbundle no_reflcl_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.Wellfounded":
   - Removed lemma wellorder.wfP_less. Use wellorder.wfp_on_less instead.
     Minor INCOMPATIBILITIES.
diff -r 28ef01901650 -r 92768949a923 src/Benchmarks/Quickcheck_Benchmark/Needham_Schroeder_Base.thy
--- a/src/Benchmarks/Quickcheck_Benchmark/Needham_Schroeder_Base.thy	Wed Oct 02 18:32:36 2024 +0200
+++ b/src/Benchmarks/Quickcheck_Benchmark/Needham_Schroeder_Base.thy	Thu Oct 03 13:01:31 2024 +0200
@@ -28,8 +28,6 @@
 
 syntax
   "_MTuple" :: "['a, args] \<Rightarrow> 'a * 'b"  (\<open>(\<open>indent=2 notation=\<open>mixfix message tuple\<close>\<close>\<lbrace>_,/ _\<rbrace>)\<close>)
-syntax_consts
-  MPair
 translations
   "\<lbrace>x, y, z\<rbrace>" \<rightleftharpoons> "\<lbrace>x, \<lbrace>y, z\<rbrace>\<rbrace>"
   "\<lbrace>x, y\<rbrace>" \<rightleftharpoons> "CONST MPair x y"
diff -r 28ef01901650 -r 92768949a923 src/CCL/Set.thy
--- a/src/CCL/Set.thy	Wed Oct 02 18:32:36 2024 +0200
+++ b/src/CCL/Set.thy	Thu Oct 03 13:01:31 2024 +0200
@@ -19,8 +19,6 @@
 
 syntax
   "_Coll" :: "[idt, o] \<Rightarrow> 'a set"  (\<open>(\<open>indent=1 notation=\<open>mixfix Collect\<close>\<close>{_./ _})\<close>)
-syntax_consts
-  Collect
 translations
   "{x. P}" == "CONST Collect(\<lambda>x. P)"
 
diff -r 28ef01901650 -r 92768949a923 src/CCL/Term.thy
--- a/src/CCL/Term.thy	Wed Oct 02 18:32:36 2024 +0200
+++ b/src/CCL/Term.thy	Thu Oct 03 13:01:31 2024 +0200
@@ -51,7 +51,6 @@
 
 syntax "_let1" :: "[idt,i,i]\<Rightarrow>i"
   (\<open>(\<open>indent=3 notation=\<open>mixfix let be in\<close>\<close>let _ be _/ in _)\<close> [0,0,60] 60)
-syntax_consts let1
 translations "let x be a in e" == "CONST let1(a, \<lambda>x. e)"
 
 definition letrec :: "[[i,i\<Rightarrow>i]\<Rightarrow>i,(i\<Rightarrow>i)\<Rightarrow>i]\<Rightarrow>i"
@@ -73,7 +72,6 @@
     (\<open>(\<open>indent=3 notation=\<open>mixfix letrec be in\<close>\<close>letrec _ _ _ be _/ in _)\<close> [0,0,0,0,60] 60)
   "_letrec3" :: "[idt,idt,idt,idt,i,i]\<Rightarrow>i"
     (\<open>(\<open>indent=3 notation=\<open>mixfix letrec be in\<close>\<close>letrec _ _ _ _ be _/ in _)\<close> [0,0,0,0,0,60] 60)
-syntax_consts letrec letrec2 letrec3
 parse_translation \<open>
   let
     fun abs_tr t u = Syntax_Trans.abs_tr [t, u];
diff -r 28ef01901650 -r 92768949a923 src/CCL/Type.thy
--- a/src/CCL/Type.thy	Wed Oct 02 18:32:36 2024 +0200
+++ b/src/CCL/Type.thy	Thu Oct 03 13:01:31 2024 +0200
@@ -14,8 +14,6 @@
 
 syntax
   "_Subtype" :: "[idt, 'a set, o] \<Rightarrow> 'a set"  (\<open>(\<open>indent=1 notation=\<open>mixfix Subtype\<close>\<close>{_: _ ./ _})\<close>)
-syntax_consts
-  Subtype
 translations
   "{x: A. B}" == "CONST Subtype(A, \<lambda>x. B)"
 
diff -r 28ef01901650 -r 92768949a923 src/Doc/Datatypes/Datatypes.thy
--- a/src/Doc/Datatypes/Datatypes.thy	Wed Oct 02 18:32:36 2024 +0200
+++ b/src/Doc/Datatypes/Datatypes.thy	Thu Oct 03 13:01:31 2024 +0200
@@ -453,8 +453,7 @@
 Incidentally, this is how the traditional syntax can be set up:
 \<close>
 (*<*)
-no_syntax
-  "_list" :: "args => 'a list"    (\<open>[(\<open>notation=\<open>mixfix list enumeration\<close>\<close>_)]\<close>)
+unbundle no_list_syntax
 (*>*)
     syntax "_list" :: "args \<Rightarrow> 'a list" (\<open>[(_)]\<close>)
 
diff -r 28ef01901650 -r 92768949a923 src/Doc/Isar_Ref/Spec.thy
--- a/src/Doc/Isar_Ref/Spec.thy	Wed Oct 02 18:32:36 2024 +0200
+++ b/src/Doc/Isar_Ref/Spec.thy	Thu Oct 03 13:01:31 2024 +0200
@@ -231,7 +231,7 @@
   (\secref{sec:locale}).
 
   \<^rail>\<open>
-    @@{command bundle} @{syntax name}
+    (@@{command bundle} | @@{command open_bundle}) @{syntax name} \<newline>
       ( '=' @{syntax thms} @{syntax for_fixes} | @'begin')
     ;
     @@{command print_bundles} ('!'?)
@@ -258,6 +258,9 @@
   b\<close>'' or ``\<^theory_text>\<open>lemma a [simp]: B \<proof>\<close>'' are also admitted, but the name
   bindings are not recorded in the bundle.
 
+  \<^descr> \<^theory_text>\<open>open_bundle b\<close> is like \<^theory_text>\<open>bundle b\<close> followed by \<^theory_text>\<open>unbundle b\<close>, so its
+  declarations are applied immediately, but also named for later re-use.
+
   \<^descr> \<^theory_text>\<open>print_bundles\<close> prints the named bundles that are available in the
   current context; the ``\<open>!\<close>'' option indicates extra verbosity.
 
diff -r 28ef01901650 -r 92768949a923 src/Doc/Tutorial/Protocol/Message.thy
--- a/src/Doc/Tutorial/Protocol/Message.thy	Wed Oct 02 18:32:36 2024 +0200
+++ b/src/Doc/Tutorial/Protocol/Message.thy	Thu Oct 03 13:01:31 2024 +0200
@@ -81,8 +81,6 @@
 text\<open>Concrete syntax: messages appear as \<open>\<lbrace>A,B,NA\<rbrace>\<close>, etc...\<close>
 syntax
   "_MTuple" :: "['a, args] \<Rightarrow> 'a * 'b"  ("(\<open>indent=2 notation=\<open>mixfix message tuple\<close>\<close>\<lbrace>_,/ _\<rbrace>)")
-syntax_consts
-  MPair
 translations
   "\<lbrace>x, y, z\<rbrace>" \<rightleftharpoons> "\<lbrace>x, \<lbrace>y, z\<rbrace>\<rbrace>"
   "\<lbrace>x, y\<rbrace>" \<rightleftharpoons> "CONST MPair x y"
diff -r 28ef01901650 -r 92768949a923 src/FOL/IFOL.thy
--- a/src/FOL/IFOL.thy	Wed Oct 02 18:32:36 2024 +0200
+++ b/src/FOL/IFOL.thy	Thu Oct 03 13:01:31 2024 +0200
@@ -747,8 +747,6 @@
   ""            :: \<open>letbind => letbinds\<close>              (\<open>_\<close>)
   "_binds"      :: \<open>[letbind, letbinds] => letbinds\<close>  (\<open>_;/ _\<close>)
   "_Let"        :: \<open>[letbinds, 'a] => 'a\<close>  (\<open>(\<open>notation=\<open>mixfix let in\<close>\<close>let (_)/ in (_))\<close> 10)
-syntax_consts
-  Let
 translations
   "_Let(_binds(b, bs), e)"  == "_Let(b, _Let(bs, e))"
   "let x = a in e"          == "CONST Let(a, \<lambda>x. e)"
diff -r 28ef01901650 -r 92768949a923 src/HOL/Analysis/Bochner_Integration.thy
--- a/src/HOL/Analysis/Bochner_Integration.thy	Wed Oct 02 18:32:36 2024 +0200
+++ b/src/HOL/Analysis/Bochner_Integration.thy	Thu Oct 03 13:01:31 2024 +0200
@@ -890,7 +890,8 @@
   "integral\<^sup>L M f = (if \<exists>x. has_bochner_integral M f x then THE x. has_bochner_integral M f x else 0)"
 
 syntax
-  "_lebesgue_integral" :: "pttrn \<Rightarrow> real \<Rightarrow> 'a measure \<Rightarrow> real" (\<open>\<integral>((2 _./ _)/ \<partial>_)\<close> [60,61] 110)
+  "_lebesgue_integral" :: "pttrn \<Rightarrow> real \<Rightarrow> 'a measure \<Rightarrow> real"
+    (\<open>(\<open>indent=1 notation=\<open>binder integral\<close>\<close>\<integral>(2 _./ _)/ \<partial>_)\<close> [60,61] 110)
 
 syntax_consts
   "_lebesgue_integral" == lebesgue_integral
@@ -899,7 +900,8 @@
   "\<integral> x. f \<partial>M" == "CONST lebesgue_integral M (\<lambda>x. f)"
 
 syntax
-  "_ascii_lebesgue_integral" :: "pttrn \<Rightarrow> 'a measure \<Rightarrow> real \<Rightarrow> real" (\<open>(3LINT (1_)/|(_)./ _)\<close> [0,110,60] 60)
+  "_ascii_lebesgue_integral" :: "pttrn \<Rightarrow> 'a measure \<Rightarrow> real \<Rightarrow> real"
+    (\<open>(\<open>indent=3 notation=\<open>mixfix LINT\<close>\<close>LINT (1_)/|(_)./ _)\<close> [0,110,60] 60)
 
 syntax_consts
   "_ascii_lebesgue_integral" == lebesgue_integral
diff -r 28ef01901650 -r 92768949a923 src/HOL/Analysis/Bounded_Continuous_Function.thy
--- a/src/HOL/Analysis/Bounded_Continuous_Function.thy	Wed Oct 02 18:32:36 2024 +0200
+++ b/src/HOL/Analysis/Bounded_Continuous_Function.thy	Thu Oct 03 13:01:31 2024 +0200
@@ -10,7 +10,7 @@
 
 definition\<^marker>\<open>tag important\<close> "bcontfun = {f. continuous_on UNIV f \<and> bounded (range f)}"
 
-typedef (overloaded) ('a, 'b) bcontfun (\<open>(_ \<Rightarrow>\<^sub>C /_)\<close> [22, 21] 21) =
+typedef (overloaded) ('a, 'b) bcontfun (\<open>(\<open>notation=\<open>infix \<Rightarrow>\<^sub>C\<close>\<close>_ \<Rightarrow>\<^sub>C /_)\<close> [22, 21] 21) =
   "bcontfun::('a::topological_space \<Rightarrow> 'b::metric_space) set"
   morphisms apply_bcontfun Bcontfun
   by (auto intro: continuous_intros simp: bounded_def bcontfun_def)
diff -r 28ef01901650 -r 92768949a923 src/HOL/Analysis/Bounded_Linear_Function.thy
--- a/src/HOL/Analysis/Bounded_Linear_Function.thy	Wed Oct 02 18:32:36 2024 +0200
+++ b/src/HOL/Analysis/Bounded_Linear_Function.thy	Thu Oct 03 13:01:31 2024 +0200
@@ -116,7 +116,7 @@
 
 subsection \<open>Type of bounded linear functions\<close>
 
-typedef\<^marker>\<open>tag important\<close> (overloaded) ('a, 'b) blinfun (\<open>(_ \<Rightarrow>\<^sub>L /_)\<close> [22, 21] 21) =
+typedef\<^marker>\<open>tag important\<close> (overloaded) ('a, 'b) blinfun (\<open>(\<open>notation=\<open>infix \<Rightarrow>\<^sub>L\<close>\<close>_ \<Rightarrow>\<^sub>L /_)\<close> [22, 21] 21) =
   "{f::'a::real_normed_vector\<Rightarrow>'b::real_normed_vector. bounded_linear f}"
   morphisms blinfun_apply Blinfun
   by (blast intro: bounded_linear_intros)
diff -r 28ef01901650 -r 92768949a923 src/HOL/Analysis/Cross3.thy
--- a/src/HOL/Analysis/Cross3.thy	Wed Oct 02 18:32:36 2024 +0200
+++ b/src/HOL/Analysis/Cross3.thy	Thu Oct 03 13:01:31 2024 +0200
@@ -21,12 +21,14 @@
 
 end
 
-bundle cross3_syntax begin
+bundle cross3_syntax
+begin
 notation cross3 (infixr \<open>\<times>\<close> 80)
 no_notation Product_Type.Times (infixr \<open>\<times>\<close> 80)
 end
 
-bundle no_cross3_syntax begin
+bundle no_cross3_syntax
+begin
 no_notation cross3 (infixr \<open>\<times>\<close> 80)
 notation Product_Type.Times (infixr \<open>\<times>\<close> 80)
 end
diff -r 28ef01901650 -r 92768949a923 src/HOL/Analysis/Finite_Cartesian_Product.thy
--- a/src/HOL/Analysis/Finite_Cartesian_Product.thy	Wed Oct 02 18:32:36 2024 +0200
+++ b/src/HOL/Analysis/Finite_Cartesian_Product.thy	Thu Oct 03 13:01:31 2024 +0200
@@ -20,20 +20,16 @@
 
 declare vec_lambda_inject [simplified, simp]
 
-bundle vec_syntax begin
-notation
-  vec_nth (infixl \<open>$\<close> 90) and
-  vec_lambda (binder \<open>\<chi>\<close> 10)
+open_bundle vec_syntax
+begin
+notation vec_nth (infixl \<open>$\<close> 90) and vec_lambda (binder \<open>\<chi>\<close> 10)
 end
 
-bundle no_vec_syntax begin
-no_notation
-  vec_nth (infixl \<open>$\<close> 90) and
-  vec_lambda (binder \<open>\<chi>\<close> 10)
+bundle no_vec_syntax
+begin
+no_notation vec_nth (infixl \<open>$\<close> 90) and vec_lambda (binder \<open>\<chi>\<close> 10)
 end
 
-unbundle vec_syntax
-
 text \<open>
   Concrete syntax for \<open>('a, 'b) vec\<close>:
     \<^item> \<open>'a^'b\<close> becomes \<open>('a, 'b::finite) vec\<close>
diff -r 28ef01901650 -r 92768949a923 src/HOL/Analysis/Finite_Product_Measure.thy
--- a/src/HOL/Analysis/Finite_Product_Measure.thy	Wed Oct 02 18:32:36 2024 +0200
+++ b/src/HOL/Analysis/Finite_Product_Measure.thy	Thu Oct 03 13:01:31 2024 +0200
@@ -169,7 +169,8 @@
   "Pi\<^sub>M I M \<equiv> PiM I M"
 
 syntax
-  "_PiM" :: "pttrn \<Rightarrow> 'i set \<Rightarrow> 'a measure \<Rightarrow> ('i => 'a) measure"  (\<open>(3\<Pi>\<^sub>M _\<in>_./ _)\<close>  10)
+  "_PiM" :: "pttrn \<Rightarrow> 'i set \<Rightarrow> 'a measure \<Rightarrow> ('i => 'a) measure"
+    (\<open>(\<open>indent=3 notation=\<open>binder \<Pi>\<^sub>M\<close>\<close>\<Pi>\<^sub>M _\<in>_./ _)\<close>  10)
 syntax_consts
   "_PiM" == PiM
 translations
diff -r 28ef01901650 -r 92768949a923 src/HOL/Analysis/Infinite_Set_Sum.thy
--- a/src/HOL/Analysis/Infinite_Set_Sum.thy	Wed Oct 02 18:32:36 2024 +0200
+++ b/src/HOL/Analysis/Infinite_Set_Sum.thy	Thu Oct 03 13:01:31 2024 +0200
@@ -96,10 +96,10 @@
 
 syntax (ASCII)
   "_infsetsum" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b::{banach, second_countable_topology}"
-  (\<open>(3INFSETSUM _:_./ _)\<close> [0, 51, 10] 10)
+  (\<open>(\<open>indent=3 notation=\<open>binder INFSETSUM\<close>\<close>INFSETSUM _:_./ _)\<close> [0, 51, 10] 10)
 syntax
   "_infsetsum" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b::{banach, second_countable_topology}"
-  (\<open>(2\<Sum>\<^sub>a_\<in>_./ _)\<close> [0, 51, 10] 10)
+  (\<open>(\<open>indent=2 notation=\<open>binder \<Sum>\<^sub>a\<close>\<close>\<Sum>\<^sub>a_\<in>_./ _)\<close> [0, 51, 10] 10)
 syntax_consts
   "_infsetsum" \<rightleftharpoons> infsetsum
 translations \<comment> \<open>Beware of argument permutation!\<close>
@@ -107,10 +107,10 @@
 
 syntax (ASCII)
   "_uinfsetsum" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b::{banach, second_countable_topology}"
-  (\<open>(3INFSETSUM _:_./ _)\<close> [0, 51, 10] 10)
+  (\<open>(\<open>indent=3 notation=\<open>binder INFSETSUM\<close>\<close>INFSETSUM _:_./ _)\<close> [0, 51, 10] 10)
 syntax
   "_uinfsetsum" :: "pttrn \<Rightarrow> 'b \<Rightarrow> 'b::{banach, second_countable_topology}"
-  (\<open>(2\<Sum>\<^sub>a_./ _)\<close> [0, 10] 10)
+  (\<open>(\<open>indent=2 notation=\<open>binder \<Sum>\<^sub>a\<close>\<close>\<Sum>\<^sub>a_./ _)\<close> [0, 10] 10)
 syntax_consts
   "_uinfsetsum" \<rightleftharpoons> infsetsum
 translations \<comment> \<open>Beware of argument permutation!\<close>
@@ -118,10 +118,10 @@
 
 syntax (ASCII)
   "_qinfsetsum" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a::{banach, second_countable_topology}"
-  (\<open>(3INFSETSUM _ |/ _./ _)\<close> [0, 0, 10] 10)
+  (\<open>(\<open>indent=3 notation=\<open>binder INFSETSUM\<close>\<close>INFSETSUM _ |/ _./ _)\<close> [0, 0, 10] 10)
 syntax
   "_qinfsetsum" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a::{banach, second_countable_topology}"
-  (\<open>(2\<Sum>\<^sub>a_ | (_)./ _)\<close> [0, 0, 10] 10)
+  (\<open>(\<open>indent=2 notation=\<open>binder \<Sum>\<^sub>a\<close>\<close>\<Sum>\<^sub>a_ | (_)./ _)\<close> [0, 0, 10] 10)
 syntax_consts
   "_qinfsetsum" \<rightleftharpoons> infsetsum
 translations
diff -r 28ef01901650 -r 92768949a923 src/HOL/Analysis/Infinite_Sum.thy
--- a/src/HOL/Analysis/Infinite_Sum.thy	Wed Oct 02 18:32:36 2024 +0200
+++ b/src/HOL/Analysis/Infinite_Sum.thy	Thu Oct 03 13:01:31 2024 +0200
@@ -47,27 +47,29 @@
   "f abs_summable_on A \<equiv> (\<lambda>x. norm (f x)) summable_on A"
 
 syntax (ASCII)
-  "_infsum" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b::topological_comm_monoid_add"  (\<open>(3INFSUM (_/:_)./ _)\<close> [0, 51, 10] 10)
+  "_infsum" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b::topological_comm_monoid_add"
+    (\<open>(\<open>indent=3 notation=\<open>binder INFSUM\<close>\<close>INFSUM (_/:_)./ _)\<close> [0, 51, 10] 10)
 syntax
-  "_infsum" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b::topological_comm_monoid_add"  (\<open>(2\<Sum>\<^sub>\<infinity>(_/\<in>_)./ _)\<close> [0, 51, 10] 10)
+  "_infsum" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b::topological_comm_monoid_add"
+    (\<open>(\<open>indent=2 notation=\<open>binder \<Sum>\<^sub>\<infinity>\<close>\<close>\<Sum>\<^sub>\<infinity>(_/\<in>_)./ _)\<close> [0, 51, 10] 10)
 syntax_consts
   "_infsum" \<rightleftharpoons> infsum
 translations \<comment> \<open>Beware of argument permutation!\<close>
   "\<Sum>\<^sub>\<infinity>i\<in>A. b" \<rightleftharpoons> "CONST infsum (\<lambda>i. b) A"
 
 syntax (ASCII)
-  "_univinfsum" :: "pttrn \<Rightarrow> 'a \<Rightarrow> 'a"  (\<open>(3INFSUM _./ _)\<close> [0, 10] 10)
+  "_univinfsum" :: "pttrn \<Rightarrow> 'a \<Rightarrow> 'a"  (\<open>(\<open>indent=3 notation=\<open>binder INFSUM\<close>\<close>INFSUM _./ _)\<close> [0, 10] 10)
 syntax
-  "_univinfsum" :: "pttrn \<Rightarrow> 'a \<Rightarrow> 'a"  (\<open>(2\<Sum>\<^sub>\<infinity>_./ _)\<close> [0, 10] 10)
+  "_univinfsum" :: "pttrn \<Rightarrow> 'a \<Rightarrow> 'a"  (\<open>(\<open>indent=2 notation=\<open>binder \<Sum>\<^sub>\<infinity>\<close>\<close>\<Sum>\<^sub>\<infinity>_./ _)\<close> [0, 10] 10)
 syntax_consts
   "_univinfsum" \<rightleftharpoons> infsum
 translations
   "\<Sum>\<^sub>\<infinity>x. t" \<rightleftharpoons> "CONST infsum (\<lambda>x. t) (CONST UNIV)"
 
 syntax (ASCII)
-  "_qinfsum" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a"  (\<open>(3INFSUM _ |/ _./ _)\<close> [0, 0, 10] 10)
+  "_qinfsum" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a"  (\<open>(\<open>indent=3 notation=\<open>binder INFSUM\<close>\<close>INFSUM _ |/ _./ _)\<close> [0, 0, 10] 10)
 syntax
-  "_qinfsum" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a"  (\<open>(2\<Sum>\<^sub>\<infinity>_ | (_)./ _)\<close> [0, 0, 10] 10)
+  "_qinfsum" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a"  (\<open>(\<open>indent=2 notation=\<open>binder \<Sum>\<^sub>\<infinity>\<close>\<close>\<Sum>\<^sub>\<infinity>_ | (_)./ _)\<close> [0, 0, 10] 10)
 syntax_consts
   "_qinfsum" \<rightleftharpoons> infsum
 translations
diff -r 28ef01901650 -r 92768949a923 src/HOL/Analysis/Inner_Product.thy
--- a/src/HOL/Analysis/Inner_Product.thy	Wed Oct 02 18:32:36 2024 +0200
+++ b/src/HOL/Analysis/Inner_Product.thy	Thu Oct 03 13:01:31 2024 +0200
@@ -391,9 +391,8 @@
 subsection \<open>Gradient derivative\<close>
 
 definition\<^marker>\<open>tag important\<close>
-  gderiv ::
-    "['a::real_inner \<Rightarrow> real, 'a, 'a] \<Rightarrow> bool"
-          (\<open>(GDERIV (_)/ (_)/ :> (_))\<close> [1000, 1000, 60] 60)
+  gderiv :: "['a::real_inner \<Rightarrow> real, 'a, 'a] \<Rightarrow> bool"
+    (\<open>(\<open>notation=\<open>mixfix GDERIV\<close>\<close>GDERIV (_)/ (_)/ :> (_))\<close> [1000, 1000, 60] 60)
 where
   "GDERIV f x :> D \<longleftrightarrow> FDERIV f x :> (\<lambda>h. inner h D)"
 
@@ -462,11 +461,13 @@
 
 lemmas has_derivative_norm = GDERIV_norm [unfolded gderiv_def]
 
-bundle inner_syntax begin
+bundle inner_syntax
+begin
 notation inner (infix \<open>\<bullet>\<close> 70)
 end
 
-bundle no_inner_syntax begin
+bundle no_inner_syntax
+begin
 no_notation inner (infix \<open>\<bullet>\<close> 70)
 end
 
diff -r 28ef01901650 -r 92768949a923 src/HOL/Analysis/Interval_Integral.thy
--- a/src/HOL/Analysis/Interval_Integral.thy	Wed Oct 02 18:32:36 2024 +0200
+++ b/src/HOL/Analysis/Interval_Integral.thy	Thu Oct 03 13:01:31 2024 +0200
@@ -146,7 +146,7 @@
 
 syntax
   "_ascii_interval_lebesgue_integral" :: "pttrn \<Rightarrow> real \<Rightarrow> real \<Rightarrow> real measure \<Rightarrow> real \<Rightarrow> real"
-  (\<open>(5LINT _=_.._|_. _)\<close> [0,60,60,61,100] 60)
+  (\<open>(\<open>indent=5 notation=\<open>binder LINT\<close>\<close>LINT _=_.._|_. _)\<close> [0,60,60,61,100] 60)
 
 syntax_consts
   "_ascii_interval_lebesgue_integral" == interval_lebesgue_integral
@@ -160,7 +160,7 @@
 
 syntax
   "_ascii_interval_lebesgue_borel_integral" :: "pttrn \<Rightarrow> real \<Rightarrow> real \<Rightarrow> real \<Rightarrow> real"
-  (\<open>(4LBINT _=_.._. _)\<close> [0,60,60,61] 60)
+  (\<open>(\<open>indent=4 notation=\<open>binder LBINT\<close>\<close>LBINT _=_.._. _)\<close> [0,60,60,61] 60)
 
 syntax_consts
   "_ascii_interval_lebesgue_borel_integral" == interval_lebesgue_integral
@@ -1049,7 +1049,7 @@
 
 
 syntax "_complex_lebesgue_borel_integral" :: "pttrn \<Rightarrow> real \<Rightarrow> complex"
-  (\<open>(2CLBINT _. _)\<close> [0,60] 60)
+  (\<open>(\<open>indent=2 notation=\<open>binder CLBINT\<close>\<close>CLBINT _. _)\<close> [0,60] 60)
 
 syntax_consts
   "_complex_lebesgue_borel_integral" == complex_lebesgue_integral
@@ -1057,7 +1057,7 @@
 translations "CLBINT x. f" == "CONST complex_lebesgue_integral CONST lborel (\<lambda>x. f)"
 
 syntax "_complex_set_lebesgue_borel_integral" :: "pttrn \<Rightarrow> real set \<Rightarrow> real \<Rightarrow> complex"
-  (\<open>(3CLBINT _:_. _)\<close> [0,60,61] 60)
+  (\<open>(\<open>indent=3 notation=\<open>binder CLBINT\<close>\<close>CLBINT _:_. _)\<close> [0,60,61] 60)
 
 syntax_consts
   "_complex_set_lebesgue_borel_integral" == complex_set_lebesgue_integral
@@ -1075,7 +1075,7 @@
 
 syntax
   "_ascii_complex_interval_lebesgue_borel_integral" :: "pttrn \<Rightarrow> ereal \<Rightarrow> ereal \<Rightarrow> real \<Rightarrow> complex"
-  (\<open>(4CLBINT _=_.._. _)\<close> [0,60,60,61] 60)
+  (\<open>(\<open>indent=4 notation=\<open>binder CLBINT\<close>\<close>CLBINT _=_.._. _)\<close> [0,60,60,61] 60)
 
 syntax_consts
   "_ascii_complex_interval_lebesgue_borel_integral" == complex_interval_lebesgue_integral
diff -r 28ef01901650 -r 92768949a923 src/HOL/Analysis/Lipschitz.thy
--- a/src/HOL/Analysis/Lipschitz.thy	Wed Oct 02 18:32:36 2024 +0200
+++ b/src/HOL/Analysis/Lipschitz.thy	Thu Oct 03 13:01:31 2024 +0200
@@ -12,15 +12,16 @@
 definition\<^marker>\<open>tag important\<close> lipschitz_on
   where "lipschitz_on C U f \<longleftrightarrow> (0 \<le> C \<and> (\<forall>x \<in> U. \<forall>y\<in>U. dist (f x) (f y) \<le> C * dist x y))"
 
-bundle lipschitz_syntax begin
+open_bundle lipschitz_syntax
+begin
 notation\<^marker>\<open>tag important\<close> lipschitz_on (\<open>_-lipschitz'_on\<close> [1000])
 end
-bundle no_lipschitz_syntax begin
+
+bundle no_lipschitz_syntax
+begin
 no_notation lipschitz_on (\<open>_-lipschitz'_on\<close> [1000])
 end
 
-unbundle lipschitz_syntax
-
 lemma lipschitz_onI: "L-lipschitz_on X f"
   if "\<And>x y. x \<in> X \<Longrightarrow> y \<in> X \<Longrightarrow> dist (f x) (f y) \<le> L * dist x y" "0 \<le> L"
   using that by (auto simp: lipschitz_on_def)
diff -r 28ef01901650 -r 92768949a923 src/HOL/Analysis/Nonnegative_Lebesgue_Integration.thy
--- a/src/HOL/Analysis/Nonnegative_Lebesgue_Integration.thy	Wed Oct 02 18:32:36 2024 +0200
+++ b/src/HOL/Analysis/Nonnegative_Lebesgue_Integration.thy	Thu Oct 03 13:01:31 2024 +0200
@@ -820,7 +820,7 @@
   "integral\<^sup>N M f = (SUP g \<in> {g. simple_function M g \<and> g \<le> f}. integral\<^sup>S M g)"
 
 syntax
-  "_nn_integral" :: "pttrn \<Rightarrow> ennreal \<Rightarrow> 'a measure \<Rightarrow> ennreal" (\<open>\<integral>\<^sup>+((2 _./ _)/ \<partial>_)\<close> [60,61] 110)
+  "_nn_integral" :: "pttrn \<Rightarrow> ennreal \<Rightarrow> 'a measure \<Rightarrow> ennreal" (\<open>(\<open>indent=2 notation=\<open>binder integral\<close>\<close>\<integral>\<^sup>+(2 _./ _)/ \<partial>_)\<close> [60,61] 110)
 
 syntax_consts
   "_nn_integral" == nn_integral
diff -r 28ef01901650 -r 92768949a923 src/HOL/Analysis/Set_Integral.thy
--- a/src/HOL/Analysis/Set_Integral.thy	Wed Oct 02 18:32:36 2024 +0200
+++ b/src/HOL/Analysis/Set_Integral.thy	Thu Oct 03 13:01:31 2024 +0200
@@ -24,7 +24,7 @@
 
 syntax
   "_ascii_set_lebesgue_integral" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'a measure \<Rightarrow> real \<Rightarrow> real"
-  (\<open>(4LINT (_):(_)/|(_)./ _)\<close> [0,0,0,10] 10)
+  (\<open>(\<open>indent=4 notation=\<open>binder LINT\<close>\<close>LINT (_):(_)/|(_)./ _)\<close> [0,0,0,10] 10)
 
 syntax_consts
   "_ascii_set_lebesgue_integral" == set_lebesgue_integral
@@ -43,11 +43,11 @@
 
 syntax
   "_lebesgue_borel_integral" :: "pttrn \<Rightarrow> real \<Rightarrow> real"
-  (\<open>(2LBINT _./ _)\<close> [0,10] 10)
+  (\<open>(\<open>indent=2 notation=\<open>binder LBINT\<close>\<close>LBINT _./ _)\<close> [0,10] 10)
 
 syntax
   "_set_lebesgue_borel_integral" :: "pttrn \<Rightarrow> real set \<Rightarrow> real \<Rightarrow> real"
-  (\<open>(3LBINT _:_./ _)\<close> [0,0,10] 10)
+  (\<open>(\<open>indent=3 notation=\<open>binder LBINT\<close>\<close>LBINT _:_./ _)\<close> [0,0,10] 10)
 
 section \<open>Basic properties\<close>
 
@@ -587,7 +587,7 @@
 
 syntax
   "_ascii_complex_lebesgue_integral" :: "pttrn \<Rightarrow> 'a measure \<Rightarrow> real \<Rightarrow> real"
-  (\<open>(3CLINT _|_. _)\<close> [0,0,10] 10)
+  (\<open>(\<open>indent=3 notation=\<open>binder CLINT\<close>\<close>CLINT _|_. _)\<close> [0,0,10] 10)
 
 syntax_consts
   "_ascii_complex_lebesgue_integral" == complex_lebesgue_integral
@@ -624,7 +624,7 @@
 
 syntax
   "_ascii_complex_set_lebesgue_integral" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'a measure \<Rightarrow> real \<Rightarrow> real"
-  (\<open>(4CLINT _:_|_. _)\<close> [0,0,0,10] 10)
+  (\<open>(\<open>indent=4 notation=\<open>binder CLINT\<close>\<close>CLINT _:_|_. _)\<close> [0,0,0,10] 10)
 
 syntax_consts
   "_ascii_complex_set_lebesgue_integral" == complex_set_lebesgue_integral
@@ -647,10 +647,10 @@
 
 syntax
 "_set_nn_integral" :: "pttrn => 'a set => 'a measure => ereal => ereal"
-(\<open>(\<integral>\<^sup>+((_)\<in>(_)./ _)/\<partial>_)\<close> [0,0,0,110] 10)
+(\<open>(\<open>notation=\<open>binder integral\<close>\<close>\<integral>\<^sup>+((_)\<in>(_)./ _)/\<partial>_)\<close> [0,0,0,110] 10)
 
 "_set_lebesgue_integral" :: "pttrn => 'a set => 'a measure => ereal => ereal"
-(\<open>(\<integral>((_)\<in>(_)./ _)/\<partial>_)\<close> [0,0,0,110] 10)
+(\<open>(\<open>notation=\<open>binder integral\<close>\<close>\<integral>((_)\<in>(_)./ _)/\<partial>_)\<close> [0,0,0,110] 10)
 
 syntax_consts
 "_set_nn_integral" == set_nn_integral and
diff -r 28ef01901650 -r 92768949a923 src/HOL/Analysis/Sparse_In.thy
--- a/src/HOL/Analysis/Sparse_In.thy	Wed Oct 02 18:32:36 2024 +0200
+++ b/src/HOL/Analysis/Sparse_In.thy	Thu Oct 03 13:01:31 2024 +0200
@@ -165,14 +165,14 @@
  "cosparse A = Abs_filter (\<lambda>P. {x. \<not>P x} sparse_in A)"
 
 syntax
-  "_eventually_cosparse" :: "pttrn => 'a set => bool => bool"  (\<open>(3\<forall>\<^sub>\<approx>_\<in>_./ _)\<close> [0, 0, 10] 10)
+  "_eventually_cosparse" :: "pttrn => 'a set => bool => bool"  (\<open>(\<open>indent=3 notation=\<open>binder \<forall>\<approx>\<close>\<close>\<forall>\<^sub>\<approx>_\<in>_./ _)\<close> [0, 0, 10] 10)
 syntax_consts
   "_eventually_cosparse" == eventually
 translations
   "\<forall>\<^sub>\<approx>x\<in>A. P" == "CONST eventually (\<lambda>x. P) (CONST cosparse A)"
 
 syntax
-  "_qeventually_cosparse" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a"  (\<open>(3\<forall>\<^sub>\<approx>_ | (_)./ _)\<close> [0, 0, 10] 10)
+  "_qeventually_cosparse" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a"  (\<open>(\<open>indent=3 notation=\<open>binder \<forall>\<approx>\<close>\<close>\<forall>\<^sub>\<approx>_ | (_)./ _)\<close> [0, 0, 10] 10)
 syntax_consts
   "_qeventually_cosparse" == eventually
 translations
diff -r 28ef01901650 -r 92768949a923 src/HOL/Auth/Message.thy
--- a/src/HOL/Auth/Message.thy	Wed Oct 02 18:32:36 2024 +0200
+++ b/src/HOL/Auth/Message.thy	Thu Oct 03 13:01:31 2024 +0200
@@ -51,8 +51,6 @@
 text\<open>Concrete syntax: messages appear as \<open>\<lbrace>A,B,NA\<rbrace>\<close>, etc...\<close>
 syntax
   "_MTuple" :: "['a, args] \<Rightarrow> 'a * 'b"  (\<open>(\<open>indent=2 notation=\<open>mixfix message tuple\<close>\<close>\<lbrace>_,/ _\<rbrace>)\<close>)
-syntax_consts
-  MPair
 translations
   "\<lbrace>x, y, z\<rbrace>" \<rightleftharpoons> "\<lbrace>x, \<lbrace>y, z\<rbrace>\<rbrace>"
   "\<lbrace>x, y\<rbrace>" \<rightleftharpoons> "CONST MPair x y"
diff -r 28ef01901650 -r 92768949a923 src/HOL/Code_Evaluation.thy
--- a/src/HOL/Code_Evaluation.thy	Wed Oct 02 18:32:36 2024 +0200
+++ b/src/HOL/Code_Evaluation.thy	Thu Oct 03 13:01:31 2024 +0200
@@ -54,10 +54,7 @@
 
 bundle term_syntax
 begin
-
-notation App (infixl \<open><\<cdot>>\<close> 70)
-  and valapp (infixl \<open>{\<cdot>}\<close> 70)
-
+notation App (infixl \<open><\<cdot>>\<close> 70) and valapp (infixl \<open>{\<cdot>}\<close> 70)
 end
 
 
diff -r 28ef01901650 -r 92768949a923 src/HOL/Codegenerator_Test/Code_Lazy_Test.thy
--- a/src/HOL/Codegenerator_Test/Code_Lazy_Test.thy	Wed Oct 02 18:32:36 2024 +0200
+++ b/src/HOL/Codegenerator_Test/Code_Lazy_Test.thy	Thu Oct 03 13:01:31 2024 +0200
@@ -24,9 +24,7 @@
 
 no_notation lazy_llist (\<open>_\<close>)
 syntax
-  "_llist" :: "args => 'a list"    (\<open>\<^bold>[(\<open>notation=\<open>mixfix lazy list enumeration\<close>\<close>_)\<^bold>]\<close>)
-syntax_consts
-  lazy_llist
+  "_llist" :: "args => 'a list"  (\<open>(\<open>indent=1 notation=\<open>mixfix lazy list enumeration\<close>\<close>\<^bold>[_\<^bold>])\<close>)
 translations
   "\<^bold>[x, xs\<^bold>]" == "x\<^bold>#\<^bold>[xs\<^bold>]"
   "\<^bold>[x\<^bold>]" == "x\<^bold>#\<^bold>[\<^bold>]"
diff -r 28ef01901650 -r 92768949a923 src/HOL/Combinatorics/Perm.thy
--- a/src/HOL/Combinatorics/Perm.thy	Wed Oct 02 18:32:36 2024 +0200
+++ b/src/HOL/Combinatorics/Perm.thy	Thu Oct 03 13:01:31 2024 +0200
@@ -792,20 +792,18 @@
 
 subsection \<open>Syntax\<close>
 
-bundle no_permutation_syntax
+open_bundle no_permutation_syntax
 begin
-  no_notation swap    (\<open>\<langle>_ \<leftrightarrow> _\<rangle>\<close>)
-  no_notation cycle   (\<open>\<langle>_\<rangle>\<close>)
-  no_notation "apply" (infixl \<open>\<langle>$\<rangle>\<close> 999)
+no_notation swap    (\<open>\<langle>_ \<leftrightarrow> _\<rangle>\<close>)
+no_notation cycle   (\<open>\<langle>_\<rangle>\<close>)
+no_notation "apply" (infixl \<open>\<langle>$\<rangle>\<close> 999)
 end
 
 bundle permutation_syntax
 begin
-  notation swap       (\<open>\<langle>_ \<leftrightarrow> _\<rangle>\<close>)
-  notation cycle      (\<open>\<langle>_\<rangle>\<close>)
-  notation "apply"    (infixl \<open>\<langle>$\<rangle>\<close> 999)
+notation swap       (\<open>\<langle>_ \<leftrightarrow> _\<rangle>\<close>)
+notation cycle      (\<open>\<langle>_\<rangle>\<close>)
+notation "apply"    (infixl \<open>\<langle>$\<rangle>\<close> 999)
 end
 
-unbundle no_permutation_syntax
-
 end
diff -r 28ef01901650 -r 92768949a923 src/HOL/Computational_Algebra/Formal_Laurent_Series.thy
--- a/src/HOL/Computational_Algebra/Formal_Laurent_Series.thy	Wed Oct 02 18:32:36 2024 +0200
+++ b/src/HOL/Computational_Algebra/Formal_Laurent_Series.thy	Thu Oct 03 13:01:31 2024 +0200
@@ -25,7 +25,7 @@
 
 setup_lifting type_definition_fls
 
-unbundle fps_notation
+unbundle fps_syntax
 notation fls_nth (infixl \<open>$$\<close> 75)
 
 lemmas fls_eqI = iffD1[OF fls_nth_inject, OF iffD2, OF fun_eq_iff, OF allI]
@@ -4603,7 +4603,7 @@
 
 no_notation fls_nth (infixl \<open>$$\<close> 75)
 
-bundle fls_notation
+bundle fps_syntax
 begin
 notation fls_nth (infixl \<open>$$\<close> 75)
 end
diff -r 28ef01901650 -r 92768949a923 src/HOL/Computational_Algebra/Formal_Power_Series.thy
--- a/src/HOL/Computational_Algebra/Formal_Power_Series.thy	Wed Oct 02 18:32:36 2024 +0200
+++ b/src/HOL/Computational_Algebra/Formal_Power_Series.thy	Thu Oct 03 13:01:31 2024 +0200
@@ -6193,7 +6193,7 @@
 (* TODO: Figure out better notation for this thing *)
 no_notation fps_nth (infixl \<open>$\<close> 75)
 
-bundle fps_notation
+bundle fps_syntax
 begin
 notation fps_nth (infixl \<open>$\<close> 75)
 end
diff -r 28ef01901650 -r 92768949a923 src/HOL/Computational_Algebra/Polynomial.thy
--- a/src/HOL/Computational_Algebra/Polynomial.thy	Wed Oct 02 18:32:36 2024 +0200
+++ b/src/HOL/Computational_Algebra/Polynomial.thy	Thu Oct 03 13:01:31 2024 +0200
@@ -349,9 +349,7 @@
 subsection \<open>List-style syntax for polynomials\<close>
 
 syntax
-  "_poly" :: "args \<Rightarrow> 'a poly"  (\<open>[:(\<open>notation=\<open>mixfix polynomial enumeration\<close>\<close>_):]\<close>)
-syntax_consts
-  pCons
+  "_poly" :: "args \<Rightarrow> 'a poly"  (\<open>(\<open>indent=2 notation=\<open>mixfix polynomial enumeration\<close>\<close>[:_:])\<close>)
 translations
   "[:x, xs:]" \<rightleftharpoons> "CONST pCons x [:xs:]"
   "[:x:]" \<rightleftharpoons> "CONST pCons x 0"
diff -r 28ef01901650 -r 92768949a923 src/HOL/Computational_Algebra/Polynomial_FPS.thy
--- a/src/HOL/Computational_Algebra/Polynomial_FPS.thy	Wed Oct 02 18:32:36 2024 +0200
+++ b/src/HOL/Computational_Algebra/Polynomial_FPS.thy	Thu Oct 03 13:01:31 2024 +0200
@@ -9,7 +9,7 @@
 begin
 
 context
-  includes fps_notation
+  includes fps_syntax
 begin
 
 definition fps_of_poly where
diff -r 28ef01901650 -r 92768949a923 src/HOL/Decision_Procs/Approximation.thy
--- a/src/HOL/Decision_Procs/Approximation.thy	Wed Oct 02 18:32:36 2024 +0200
+++ b/src/HOL/Decision_Procs/Approximation.thy	Thu Oct 03 13:01:31 2024 +0200
@@ -1143,7 +1143,8 @@
 
 section "Avoid pollution of name space"
 
-bundle floatarith_notation begin
+bundle floatarith_syntax
+begin
 
 notation Add (\<open>Add\<close>)
 notation Minus (\<open>Minus\<close>)
@@ -1166,7 +1167,8 @@
 
 end
 
-bundle no_floatarith_notation begin
+bundle no_floatarith_syntax
+begin
 
 no_notation Add (\<open>Add\<close>)
 no_notation Minus (\<open>Minus\<close>)
diff -r 28ef01901650 -r 92768949a923 src/HOL/Fun.thy
--- a/src/HOL/Fun.thy	Wed Oct 02 18:32:36 2024 +0200
+++ b/src/HOL/Fun.thy	Thu Oct 03 13:01:31 2024 +0200
@@ -846,9 +846,6 @@
   "_updbinds":: "updbind \<Rightarrow> updbinds \<Rightarrow> updbinds" (\<open>_,/ _\<close>)
   "_Update"  :: "'a \<Rightarrow> updbinds \<Rightarrow> 'a"            (\<open>_/'((2_)')\<close> [1000, 0] 900)
 
-syntax_consts
-  fun_upd
-
 translations
   "_Update f (_updbinds b bs)" \<rightleftharpoons> "_Update (_Update f b) bs"
   "f(x:=y)" \<rightleftharpoons> "CONST fun_upd f x y"
diff -r 28ef01901650 -r 92768949a923 src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Wed Oct 02 18:32:36 2024 +0200
+++ b/src/HOL/HOL.thy	Thu Oct 03 13:01:31 2024 +0200
@@ -191,11 +191,11 @@
 nonterminal case_syn and cases_syn
 syntax
   "_case_syntax" :: "['a, cases_syn] \<Rightarrow> 'b"  (\<open>(\<open>notation=\<open>mixfix case expression\<close>\<close>case _ of/ _)\<close> 10)
-  "_case1" :: "['a, 'b] \<Rightarrow> case_syn"  (\<open>(\<open>indent=2 notation=\<open>mixfix case pattern\<close>\<close>_ \<Rightarrow>/ _)\<close> 10)
+  "_case1" :: "['a, 'b] \<Rightarrow> case_syn"  (\<open>(\<open>indent=2 notation=\<open>mixfix case clause\<close>\<close>_ \<Rightarrow>/ _)\<close> 10)
   "" :: "case_syn \<Rightarrow> cases_syn"  (\<open>_\<close>)
   "_case2" :: "[case_syn, cases_syn] \<Rightarrow> cases_syn"  (\<open>_/ | _\<close>)
 syntax (ASCII)
-  "_case1" :: "['a, 'b] \<Rightarrow> case_syn"  (\<open>(\<open>indent=2 notation=\<open>mixfix case pattern\<close>\<close>_ =>/ _)\<close> 10)
+  "_case1" :: "['a, 'b] \<Rightarrow> case_syn"  (\<open>(\<open>indent=2 notation=\<open>mixfix case clause\<close>\<close>_ =>/ _)\<close> 10)
 
 notation (ASCII)
   All  (binder \<open>ALL \<close> 10) and
diff -r 28ef01901650 -r 92768949a923 src/HOL/HOLCF/Cfun.thy
--- a/src/HOL/HOLCF/Cfun.thy	Wed Oct 02 18:32:36 2024 +0200
+++ b/src/HOL/HOLCF/Cfun.thy	Thu Oct 03 13:01:31 2024 +0200
@@ -16,17 +16,17 @@
 
 definition "cfun = {f::'a \<Rightarrow> 'b. cont f}"
 
-cpodef ('a, 'b) cfun (\<open>(_ \<rightarrow>/ _)\<close> [1, 0] 0) = "cfun :: ('a \<Rightarrow> 'b) set"
+cpodef ('a, 'b) cfun (\<open>(\<open>notation=\<open>infix \<rightarrow>\<close>\<close>_ \<rightarrow>/ _)\<close> [1, 0] 0) = "cfun :: ('a \<Rightarrow> 'b) set"
   by (auto simp: cfun_def intro: cont_const adm_cont)
 
 type_notation (ASCII)
   cfun  (infixr \<open>->\<close> 0)
 
 notation (ASCII)
-  Rep_cfun  (\<open>(_$/_)\<close> [999,1000] 999)
+  Rep_cfun  (\<open>(\<open>notation=\<open>infix $\<close>\<close>_$/_)\<close> [999,1000] 999)
 
 notation
-  Rep_cfun  (\<open>(_\<cdot>/_)\<close> [999,1000] 999)
+  Rep_cfun  (\<open>(\<open>notation=\<open>infix \<cdot>\<close>\<close>_\<cdot>/_)\<close> [999,1000] 999)
 
 
 subsection \<open>Syntax for continuous lambda abstraction\<close>
@@ -47,10 +47,10 @@
 text \<open>Syntax for nested abstractions\<close>
 
 syntax (ASCII)
-  "_Lambda" :: "[cargs, logic] \<Rightarrow> logic"  (\<open>(3LAM _./ _)\<close> [1000, 10] 10)
+  "_Lambda" :: "[cargs, logic] \<Rightarrow> logic"  (\<open>(\<open>indent=3 notation=\<open>binder LAM\<close>\<close>LAM _./ _)\<close> [1000, 10] 10)
 
 syntax
-  "_Lambda" :: "[cargs, logic] \<Rightarrow> logic" (\<open>(3\<Lambda> _./ _)\<close> [1000, 10] 10)
+  "_Lambda" :: "[cargs, logic] \<Rightarrow> logic" (\<open>(\<open>indent=3 notation=\<open>binder \<Lambda>\<close>\<close>\<Lambda> _./ _)\<close> [1000, 10] 10)
 
 syntax_consts
   "_Lambda" \<rightleftharpoons> Abs_cfun
diff -r 28ef01901650 -r 92768949a923 src/HOL/HOLCF/ConvexPD.thy
--- a/src/HOL/HOLCF/ConvexPD.thy	Wed Oct 02 18:32:36 2024 +0200
+++ b/src/HOL/HOLCF/ConvexPD.thy	Thu Oct 03 13:01:31 2024 +0200
@@ -119,7 +119,7 @@
 
 subsection \<open>Type definition\<close>
 
-typedef 'a convex_pd  (\<open>('(_')\<natural>)\<close>) =
+typedef 'a convex_pd  (\<open>(\<open>notation=\<open>postfix convex_pd\<close>\<close>'(_')\<natural>)\<close>) =
   "{S::'a pd_basis set. convex_le.ideal S}"
 by (rule convex_le.ex_ideal)
 
@@ -178,13 +178,8 @@
     (infixl \<open>\<union>\<natural>\<close> 65) where
   "xs \<union>\<natural> ys == convex_plus\<cdot>xs\<cdot>ys"
 
-nonterminal convex_pd_args
 syntax
-  "" :: "logic \<Rightarrow> convex_pd_args"  (\<open>_\<close>)
-  "_convex_pd_args" :: "logic \<Rightarrow> convex_pd_args \<Rightarrow> convex_pd_args"  (\<open>_,/ _\<close>)
-  "_convex_pd" :: "convex_pd_args \<Rightarrow> logic"  (\<open>{_}\<natural>\<close>)
-syntax_consts
-  "_convex_pd_args" "_convex_pd" == convex_add
+  "_convex_pd" :: "args \<Rightarrow> logic"  (\<open>(\<open>indent=1 notation=\<open>mixfix convex_pd enumeration\<close>\<close>{_}\<natural>)\<close>)
 translations
   "{x,xs}\<natural>" == "{x}\<natural> \<union>\<natural> {xs}\<natural>"
   "{x}\<natural>" == "CONST convex_unit\<cdot>x"
@@ -350,10 +345,7 @@
 
 syntax
   "_convex_bind" :: "[logic, logic, logic] \<Rightarrow> logic"
-    (\<open>(3\<Union>\<natural>_\<in>_./ _)\<close> [0, 0, 10] 10)
-
-syntax_consts
-  "_convex_bind" == convex_bind
+    (\<open>(\<open>indent=3 notation=\<open>binder convex_bind\<close>\<close>\<Union>\<natural>_\<in>_./ _)\<close> [0, 0, 10] 10)
 
 translations
   "\<Union>\<natural>x\<in>xs. e" == "CONST convex_bind\<cdot>xs\<cdot>(\<Lambda> x. e)"
diff -r 28ef01901650 -r 92768949a923 src/HOL/HOLCF/FOCUS/Fstream.thy
--- a/src/HOL/HOLCF/FOCUS/Fstream.thy	Wed Oct 02 18:32:36 2024 +0200
+++ b/src/HOL/HOLCF/FOCUS/Fstream.thy	Thu Oct 03 13:01:31 2024 +0200
@@ -29,16 +29,16 @@
   "<> == \<bottom>"
 
 abbreviation
-  fscons'       :: "'a \<Rightarrow> 'a fstream \<Rightarrow> 'a fstream"       (\<open>(_\<leadsto>_)\<close> [66,65] 65) where
+  fscons'       :: "'a \<Rightarrow> 'a fstream \<Rightarrow> 'a fstream"       (\<open>(\<open>notation=\<open>infix \<leadsto>\<close>\<close>_\<leadsto>_)\<close> [66,65] 65) where
   "a\<leadsto>s == fscons a\<cdot>s"
 
 abbreviation
-  fsfilter'     :: "'a set \<Rightarrow> 'a fstream \<Rightarrow> 'a fstream"   (\<open>(_\<copyright>_)\<close> [64,63] 63) where
+  fsfilter'     :: "'a set \<Rightarrow> 'a fstream \<Rightarrow> 'a fstream"   (\<open>(\<open>notation=\<open>infix \<copyright>\<close>\<close>_\<copyright>_)\<close> [64,63] 63) where
   "A\<copyright>s == fsfilter A\<cdot>s"
 
 notation (ASCII)
-  fscons'  (\<open>(_~>_)\<close> [66,65] 65) and
-  fsfilter'  (\<open>(_'(C')_)\<close> [64,63] 63)
+  fscons'  (\<open>(\<open>notation=\<open>infix ~>\<close>\<close>_~>_)\<close> [66,65] 65) and
+  fsfilter'  (\<open>(\<open>notation=\<open>infix (C)\<close>\<close>_'(C')_)\<close> [64,63] 63)
 
 
 lemma Def_maximal: "a = Def d \<Longrightarrow> a\<sqsubseteq>b \<Longrightarrow> b = Def d"
diff -r 28ef01901650 -r 92768949a923 src/HOL/HOLCF/FOCUS/Fstreams.thy
--- a/src/HOL/HOLCF/FOCUS/Fstreams.thy	Wed Oct 02 18:32:36 2024 +0200
+++ b/src/HOL/HOLCF/FOCUS/Fstreams.thy	Thu Oct 03 13:01:31 2024 +0200
@@ -44,11 +44,11 @@
   "<> == \<bottom>"
 
 abbreviation
-  fsfilter' :: "'a set \<Rightarrow> 'a fstream \<Rightarrow> 'a fstream"       (\<open>(_\<copyright>_)\<close> [64,63] 63) where
+  fsfilter' :: "'a set \<Rightarrow> 'a fstream \<Rightarrow> 'a fstream"       (\<open>(\<open>notation=\<open>infix \<copyright>\<close>\<close>_\<copyright>_)\<close> [64,63] 63) where
   "A\<copyright>s == fsfilter A\<cdot>s"
 
 notation (ASCII)
-  fsfilter'  (\<open>(_'(C')_)\<close> [64,63] 63)
+  fsfilter'  (\<open>(\<open>notation=\<open>infix (C)\<close>\<close>_'(C')_)\<close> [64,63] 63)
 
 
 lemma ft_fsingleton[simp]: "ft\<cdot>(<a>) = Def a"
diff -r 28ef01901650 -r 92768949a923 src/HOL/HOLCF/IOA/Sequence.thy
--- a/src/HOL/HOLCF/IOA/Sequence.thy	Wed Oct 02 18:32:36 2024 +0200
+++ b/src/HOL/HOLCF/IOA/Sequence.thy	Thu Oct 03 13:01:31 2024 +0200
@@ -63,17 +63,15 @@
               UU \<Rightarrow> UU
             | Def y \<Rightarrow> (if P y then x ## (h \<cdot> xs) else h \<cdot> xs))))"
 
-abbreviation Consq_syn  (\<open>(_/\<leadsto>_)\<close> [66, 65] 65)
+abbreviation Consq_syn  (\<open>(\<open>notation=\<open>infix \<leadsto>\<close>\<close>_/\<leadsto>_)\<close> [66, 65] 65)
   where "a \<leadsto> s \<equiv> Consq a \<cdot> s"
 
 
 subsection \<open>List enumeration\<close>
 
 syntax
-  "_totlist" :: "args \<Rightarrow> 'a Seq"  (\<open>[(\<open>notation=\<open>mixfix total list enumeration\<close>\<close>_)!]\<close>)
-  "_partlist" :: "args \<Rightarrow> 'a Seq"  (\<open>[(\<open>notation=\<open>mixfix partial list enumeration\<close>\<close>_)?]\<close>)
-syntax_consts
-  Consq
+  "_totlist" :: "args \<Rightarrow> 'a Seq"  (\<open>(\<open>indent=1 notation=\<open>mixfix total list enumeration\<close>\<close>[_!])\<close>)
+  "_partlist" :: "args \<Rightarrow> 'a Seq"  (\<open>(\<open>indent=1 notation=\<open>mixfix partial list enumeration\<close>\<close>[_?])\<close>)
 translations
   "[x, xs!]" \<rightleftharpoons> "x \<leadsto> [xs!]"
   "[x!]" \<rightleftharpoons> "x\<leadsto>nil"
diff -r 28ef01901650 -r 92768949a923 src/HOL/HOLCF/IOA/TL.thy
--- a/src/HOL/HOLCF/IOA/TL.thy	Wed Oct 02 18:32:36 2024 +0200
+++ b/src/HOL/HOLCF/IOA/TL.thy	Thu Oct 03 13:01:31 2024 +0200
@@ -22,7 +22,7 @@
   where "Init P s = P (unlift (HD \<cdot> s))"
     \<comment> \<open>this means that for \<open>nil\<close> and \<open>UU\<close> the effect is unpredictable\<close>
 
-definition Next :: "'a temporal \<Rightarrow> 'a temporal"  (\<open>\<circle>(_)\<close> [80] 80)
+definition Next :: "'a temporal \<Rightarrow> 'a temporal"  (\<open>(\<open>indent=1 notation=\<open>prefix Next\<close>\<close>\<circle>_)\<close> [80] 80)
   where "(\<circle>P) s \<longleftrightarrow> (if TL \<cdot> s = UU \<or> TL \<cdot> s = nil then P s else P (TL \<cdot> s))"
 
 definition suffix :: "'a Seq \<Rightarrow> 'a Seq \<Rightarrow> bool"
@@ -31,10 +31,10 @@
 definition tsuffix :: "'a Seq \<Rightarrow> 'a Seq \<Rightarrow> bool"
   where "tsuffix s2 s \<longleftrightarrow> s2 \<noteq> nil \<and> s2 \<noteq> UU \<and> suffix s2 s"
 
-definition Box :: "'a temporal \<Rightarrow> 'a temporal"  (\<open>\<box>(_)\<close> [80] 80)
+definition Box :: "'a temporal \<Rightarrow> 'a temporal"  (\<open>(\<open>indent=1 notation=\<open>prefix Box\<close>\<close>\<box>_)\<close> [80] 80)
   where "(\<box>P) s \<longleftrightarrow> (\<forall>s2. tsuffix s2 s \<longrightarrow> P s2)"
 
-definition Diamond :: "'a temporal \<Rightarrow> 'a temporal"  (\<open>\<diamond>(_)\<close> [80] 80)
+definition Diamond :: "'a temporal \<Rightarrow> 'a temporal"  (\<open>(\<open>indent=1 notation=\<open>prefix Diamond\<close>\<close>\<diamond>_)\<close> [80] 80)
   where "\<diamond>P = (\<^bold>\<not> (\<box>(\<^bold>\<not> P)))"
 
 definition Leadsto :: "'a temporal \<Rightarrow> 'a temporal \<Rightarrow> 'a temporal"  (infixr \<open>\<leadsto>\<close> 22)
diff -r 28ef01901650 -r 92768949a923 src/HOL/HOLCF/LowerPD.thy
--- a/src/HOL/HOLCF/LowerPD.thy	Wed Oct 02 18:32:36 2024 +0200
+++ b/src/HOL/HOLCF/LowerPD.thy	Thu Oct 03 13:01:31 2024 +0200
@@ -74,7 +74,7 @@
 
 subsection \<open>Type definition\<close>
 
-typedef 'a lower_pd  (\<open>('(_')\<flat>)\<close>) =
+typedef 'a lower_pd  (\<open>(\<open>notation=\<open>postfix lower_pd\<close>\<close>'(_')\<flat>)\<close>) =
   "{S::'a pd_basis set. lower_le.ideal S}"
 by (rule lower_le.ex_ideal)
 
@@ -133,13 +133,8 @@
     (infixl \<open>\<union>\<flat>\<close> 65) where
   "xs \<union>\<flat> ys == lower_plus\<cdot>xs\<cdot>ys"
 
-nonterminal lower_pd_args
 syntax
-  "" :: "logic \<Rightarrow> lower_pd_args"  (\<open>_\<close>)
-  "_lower_pd_args" :: "logic \<Rightarrow> lower_pd_args \<Rightarrow> lower_pd_args"  (\<open>_,/ _\<close>)
-  "_lower_pd" :: "lower_pd_args \<Rightarrow> logic" (\<open>{_}\<flat>\<close>)
-syntax_consts
-  "_lower_pd_args" "_lower_pd" == lower_add
+  "_lower_pd" :: "args \<Rightarrow> logic"  (\<open>(\<open>indent=1 notation=\<open>mixfix lower_pd enumeration\<close>\<close>{_}\<flat>)\<close>)
 translations
   "{x,xs}\<flat>" == "{x}\<flat> \<union>\<flat> {xs}\<flat>"
   "{x}\<flat>" == "CONST lower_unit\<cdot>x"
@@ -344,10 +339,7 @@
 
 syntax
   "_lower_bind" :: "[logic, logic, logic] \<Rightarrow> logic"
-    (\<open>(3\<Union>\<flat>_\<in>_./ _)\<close> [0, 0, 10] 10)
-
-syntax_consts
-  "_lower_bind" == lower_bind
+    (\<open>(\<open>indent=3 notation=\<open>binder lower_bind\<close>\<close>\<Union>\<flat>_\<in>_./ _)\<close> [0, 0, 10] 10)
 
 translations
   "\<Union>\<flat>x\<in>xs. e" == "CONST lower_bind\<cdot>xs\<cdot>(\<Lambda> x. e)"
diff -r 28ef01901650 -r 92768949a923 src/HOL/HOLCF/Pcpo.thy
--- a/src/HOL/HOLCF/Pcpo.thy	Wed Oct 02 18:32:36 2024 +0200
+++ b/src/HOL/HOLCF/Pcpo.thy	Thu Oct 03 13:01:31 2024 +0200
@@ -151,10 +151,7 @@
 end
 
 text \<open>Old "UU" syntax:\<close>
-
-syntax UU :: logic
-syntax_consts UU \<rightleftharpoons> bottom
-translations "UU" \<rightharpoonup> "CONST bottom"
+abbreviation (input) "UU \<equiv> bottom"
 
 text \<open>Simproc to rewrite \<^term>\<open>\<bottom> = x\<close> to \<^term>\<open>x = \<bottom>\<close>.\<close>
 setup \<open>Reorient_Proc.add (fn \<^Const_>\<open>bottom _\<close> => true | _ => false)\<close>
diff -r 28ef01901650 -r 92768949a923 src/HOL/HOLCF/Porder.thy
--- a/src/HOL/HOLCF/Porder.thy	Wed Oct 02 18:32:36 2024 +0200
+++ b/src/HOL/HOLCF/Porder.thy	Thu Oct 03 13:01:31 2024 +0200
@@ -113,10 +113,10 @@
 end
 
 syntax (ASCII)
-  "_BLub" :: "[pttrn, 'a set, 'b] \<Rightarrow> 'b" (\<open>(3LUB _:_./ _)\<close> [0,0, 10] 10)
+  "_BLub" :: "[pttrn, 'a set, 'b] \<Rightarrow> 'b" (\<open>(\<open>indent=3 notation=\<open>binder LUB\<close>\<close>LUB _:_./ _)\<close> [0,0, 10] 10)
 
 syntax
-  "_BLub" :: "[pttrn, 'a set, 'b] \<Rightarrow> 'b" (\<open>(3\<Squnion>_\<in>_./ _)\<close> [0,0, 10] 10)
+  "_BLub" :: "[pttrn, 'a set, 'b] \<Rightarrow> 'b" (\<open>(\<open>indent=3 notation=\<open>binder \<Squnion>\<close>\<close>\<Squnion>_\<in>_./ _)\<close> [0,0, 10] 10)
 
 syntax_consts
   "_BLub" \<rightleftharpoons> lub
diff -r 28ef01901650 -r 92768949a923 src/HOL/HOLCF/Sprod.thy
--- a/src/HOL/HOLCF/Sprod.thy	Wed Oct 02 18:32:36 2024 +0200
+++ b/src/HOL/HOLCF/Sprod.thy	Thu Oct 03 13:01:31 2024 +0200
@@ -16,7 +16,7 @@
 
 definition "sprod = {p::'a \<times> 'b. p = \<bottom> \<or> (fst p \<noteq> \<bottom> \<and> snd p \<noteq> \<bottom>)}"
 
-pcpodef ('a, 'b) sprod  (\<open>(_ \<otimes>/ _)\<close> [21,20] 20) = "sprod :: ('a \<times> 'b) set"
+pcpodef ('a, 'b) sprod  (\<open>(\<open>notation=\<open>infix strict product\<close>\<close>_ \<otimes>/ _)\<close> [21,20] 20) = "sprod :: ('a \<times> 'b) set"
   by (simp_all add: sprod_def)
 
 instance sprod :: ("{chfin,pcpo}", "{chfin,pcpo}") chfin
@@ -42,8 +42,6 @@
 
 syntax
   "_stuple" :: "[logic, args] \<Rightarrow> logic"  (\<open>(\<open>indent=1 notation=\<open>mixfix strict tuple\<close>\<close>'(:_,/ _:'))\<close>)
-syntax_consts
-  spair
 translations
   "(:x, y, z:)" \<rightleftharpoons> "(:x, (:y, z:):)"
   "(:x, y:)" \<rightleftharpoons> "CONST spair\<cdot>x\<cdot>y"
diff -r 28ef01901650 -r 92768949a923 src/HOL/HOLCF/Ssum.thy
--- a/src/HOL/HOLCF/Ssum.thy	Wed Oct 02 18:32:36 2024 +0200
+++ b/src/HOL/HOLCF/Ssum.thy	Thu Oct 03 13:01:31 2024 +0200
@@ -19,7 +19,7 @@
     (fst p = TT \<and> fst (snd p) \<noteq> \<bottom> \<and> snd (snd p) = \<bottom>) \<or>
     (fst p = FF \<and> fst (snd p) = \<bottom> \<and> snd (snd p) \<noteq> \<bottom>)}"
 
-pcpodef ('a, 'b) ssum  (\<open>(_ \<oplus>/ _)\<close> [21, 20] 20) = "ssum :: (tr \<times> 'a \<times> 'b) set"
+pcpodef ('a, 'b) ssum  (\<open>(\<open>notation=\<open>infix strict sum\<close>\<close>_ \<oplus>/ _)\<close> [21, 20] 20) = "ssum :: (tr \<times> 'a \<times> 'b) set"
   by (simp_all add: ssum_def)
 
 instance ssum :: ("{chfin,pcpo}", "{chfin,pcpo}") chfin
diff -r 28ef01901650 -r 92768949a923 src/HOL/HOLCF/Tr.thy
--- a/src/HOL/HOLCF/Tr.thy	Wed Oct 02 18:32:36 2024 +0200
+++ b/src/HOL/HOLCF/Tr.thy	Thu Oct 03 13:01:31 2024 +0200
@@ -63,7 +63,7 @@
 definition tr_case :: "'a \<rightarrow> 'a \<rightarrow> tr \<rightarrow> 'a"
   where "tr_case = (\<Lambda> t e (Def b). if b then t else e)"
 
-abbreviation cifte_syn :: "[tr, 'c, 'c] \<Rightarrow> 'c"  (\<open>(If (_)/ then (_)/ else (_))\<close> [0, 0, 60] 60)
+abbreviation cifte_syn :: "[tr, 'c, 'c] \<Rightarrow> 'c"  (\<open>(\<open>notation=\<open>mixfix If expression\<close>\<close>If (_)/ then (_)/ else (_))\<close> [0, 0, 60] 60)
   where "If b then e1 else e2 \<equiv> tr_case\<cdot>e1\<cdot>e2\<cdot>b"
 
 translations
diff -r 28ef01901650 -r 92768949a923 src/HOL/HOLCF/Up.thy
--- a/src/HOL/HOLCF/Up.thy	Wed Oct 02 18:32:36 2024 +0200
+++ b/src/HOL/HOLCF/Up.thy	Thu Oct 03 13:01:31 2024 +0200
@@ -14,7 +14,7 @@
 
 subsection \<open>Definition of new type for lifting\<close>
 
-datatype 'a u  (\<open>(_\<^sub>\<bottom>)\<close> [1000] 999) = Ibottom | Iup 'a
+datatype 'a u  (\<open>(\<open>notation=\<open>postfix lifting\<close>\<close>_\<^sub>\<bottom>)\<close> [1000] 999) = Ibottom | Iup 'a
 
 primrec Ifup :: "('a \<rightarrow> 'b::pcpo) \<Rightarrow> 'a u \<Rightarrow> 'b"
   where
diff -r 28ef01901650 -r 92768949a923 src/HOL/HOLCF/UpperPD.thy
--- a/src/HOL/HOLCF/UpperPD.thy	Wed Oct 02 18:32:36 2024 +0200
+++ b/src/HOL/HOLCF/UpperPD.thy	Thu Oct 03 13:01:31 2024 +0200
@@ -72,7 +72,7 @@
 
 subsection \<open>Type definition\<close>
 
-typedef 'a upper_pd  (\<open>('(_')\<sharp>)\<close>) =
+typedef 'a upper_pd  (\<open>(\<open>notation=\<open>postfix upper_pd\<close>\<close>'(_')\<sharp>)\<close>) =
   "{S::'a pd_basis set. upper_le.ideal S}"
 by (rule upper_le.ex_ideal)
 
@@ -131,13 +131,8 @@
     (infixl \<open>\<union>\<sharp>\<close> 65) where
   "xs \<union>\<sharp> ys == upper_plus\<cdot>xs\<cdot>ys"
 
-nonterminal upper_pd_args
 syntax
-  "" :: "logic \<Rightarrow> upper_pd_args"  (\<open>_\<close>)
-  "_upper_pd_args" :: "logic \<Rightarrow> upper_pd_args \<Rightarrow> upper_pd_args"  (\<open>_,/ _\<close>)
-  "_upper_pd" :: "upper_pd_args \<Rightarrow> logic"  (\<open>{_}\<sharp>\<close>)
-syntax_consts
-  "_upper_pd_args" "_upper_pd" == upper_add
+  "_upper_pd" :: "args \<Rightarrow> logic"  (\<open>(\<open>indent=1 notation=\<open>mixfix upper_pd enumeration\<close>\<close>{_}\<sharp>)\<close>)
 translations
   "{x,xs}\<sharp>" == "{x}\<sharp> \<union>\<sharp> {xs}\<sharp>"
   "{x}\<sharp>" == "CONST upper_unit\<cdot>x"
@@ -337,10 +332,7 @@
 
 syntax
   "_upper_bind" :: "[logic, logic, logic] \<Rightarrow> logic"
-    (\<open>(3\<Union>\<sharp>_\<in>_./ _)\<close> [0, 0, 10] 10)
-
-syntax_consts
-  "_upper_bind" == upper_bind
+    (\<open>(\<open>indent=3 notation=\<open>binder upper_bind\<close>\<close>\<Union>\<sharp>_\<in>_./ _)\<close> [0, 0, 10] 10)
 
 translations
   "\<Union>\<sharp>x\<in>xs. e" == "CONST upper_bind\<cdot>xs\<cdot>(\<Lambda> x. e)"
diff -r 28ef01901650 -r 92768949a923 src/HOL/HOLCF/ex/Letrec.thy
--- a/src/HOL/HOLCF/ex/Letrec.thy	Wed Oct 02 18:32:36 2024 +0200
+++ b/src/HOL/HOLCF/ex/Letrec.thy	Thu Oct 03 13:01:31 2024 +0200
@@ -15,15 +15,12 @@
 nonterminal recbinds and recbindt and recbind
 
 syntax
-  "_recbind"  :: "[logic, logic] \<Rightarrow> recbind"         (\<open>(2_ =/ _)\<close> 10)
+  "_recbind"  :: "[logic, logic] \<Rightarrow> recbind"         (\<open>(\<open>indent=2 notation=\<open>mixfix Letrec binding\<close>\<close>_ =/ _)\<close> 10)
   ""          :: "recbind \<Rightarrow> recbindt"               (\<open>_\<close>)
   "_recbindt" :: "[recbind, recbindt] \<Rightarrow> recbindt"   (\<open>_,/ _\<close>)
   ""          :: "recbindt \<Rightarrow> recbinds"              (\<open>_\<close>)
   "_recbinds" :: "[recbindt, recbinds] \<Rightarrow> recbinds"  (\<open>_;/ _\<close>)
-  "_Letrec"   :: "[recbinds, logic] \<Rightarrow> logic"        (\<open>(Letrec (_)/ in (_))\<close> 10)
-
-syntax_consts
-  "_recbind" "_recbinds" "_recbindt" "_Letrec" == CLetrec
+  "_Letrec"   :: "[recbinds, logic] \<Rightarrow> logic"        (\<open>(\<open>notation=\<open>mixfix Letrec expression\<close>\<close>Letrec (_)/ in (_))\<close> 10)
 
 translations
   (recbindt) "x = a, (y,ys) = (b,bs)" == (recbindt) "(x,y,ys) = (a,b,bs)"
diff -r 28ef01901650 -r 92768949a923 src/HOL/HOLCF/ex/Pattern_Match.thy
--- a/src/HOL/HOLCF/ex/Pattern_Match.thy	Wed Oct 02 18:32:36 2024 +0200
+++ b/src/HOL/HOLCF/ex/Pattern_Match.thy	Thu Oct 03 13:01:31 2024 +0200
@@ -103,14 +103,14 @@
 nonterminal Case_pat and Case_syn and Cases_syn
 
 syntax
-  "_Case_syntax":: "['a, Cases_syn] => 'b"               (\<open>(Case _ of/ _)\<close> 10)
-  "_Case1"      :: "[Case_pat, 'b] => Case_syn"          (\<open>(2_ \<Rightarrow>/ _)\<close> 10)
+  "_Case_syntax":: "['a, Cases_syn] => 'b"               (\<open>(\<open>notation=\<open>mixfix Case expression\<close>\<close>Case _ of/ _)\<close> 10)
+  "_Case1"      :: "[Case_pat, 'b] => Case_syn"          (\<open>(\<open>indent=2 notation=\<open>mixfix Case clause\<close>\<close>_ \<Rightarrow>/ _)\<close> 10)
   ""            :: "Case_syn => Cases_syn"               (\<open>_\<close>)
   "_Case2"      :: "[Case_syn, Cases_syn] => Cases_syn"  (\<open>_/ | _\<close>)
   "_strip_positions" :: "'a => Case_pat"                 (\<open>_\<close>)
 
 syntax (ASCII)
-  "_Case1"      :: "[Case_pat, 'b] => Case_syn"          (\<open>(2_ =>/ _)\<close> 10)
+  "_Case1"      :: "[Case_pat, 'b] => Case_syn"          (\<open>(\<open>indent=2 notation=\<open>mixfix Case clause\<close>\<close>_ =>/ _)\<close> 10)
 
 translations
   "_Case_syntax x ms" == "CONST cases\<cdot>(ms\<cdot>x)"
diff -r 28ef01901650 -r 92768949a923 src/HOL/Library/FSet.thy
--- a/src/HOL/Library/FSet.thy	Wed Oct 02 18:32:36 2024 +0200
+++ b/src/HOL/Library/FSet.thy	Thu Oct 03 13:01:31 2024 +0200
@@ -165,9 +165,7 @@
   by simp
 
 syntax
-  "_fset" :: "args => 'a fset"  (\<open>{|(\<open>notation=\<open>mixfix finite set enumeration\<close>\<close>_)|}\<close>)
-syntax_consts
-  finsert
+  "_fset" :: "args => 'a fset"  (\<open>(\<open>indent=2 notation=\<open>mixfix finite set enumeration\<close>\<close>{|_|})\<close>)
 translations
   "{|x, xs|}" == "CONST finsert x {|xs|}"
   "{|x|}"     == "CONST finsert x {||}"
@@ -194,26 +192,49 @@
 end
 
 syntax (input)
-  "_fBall"       :: "pttrn \<Rightarrow> 'a fset \<Rightarrow> bool \<Rightarrow> bool"      (\<open>(3! (_/|:|_)./ _)\<close> [0, 0, 10] 10)
-  "_fBex"        :: "pttrn \<Rightarrow> 'a fset \<Rightarrow> bool \<Rightarrow> bool"      (\<open>(3? (_/|:|_)./ _)\<close> [0, 0, 10] 10)
+  "_fBall" :: "pttrn \<Rightarrow> 'a fset \<Rightarrow> bool \<Rightarrow> bool"  (\<open>(\<open>indent=3 notation=\<open>binder finite !\<close>\<close>! (_/|:|_)./ _)\<close> [0, 0, 10] 10)
+  "_fBex"  :: "pttrn \<Rightarrow> 'a fset \<Rightarrow> bool \<Rightarrow> bool"  (\<open>(\<open>indent=3 notation=\<open>binder finite ?\<close>\<close>? (_/|:|_)./ _)\<close> [0, 0, 10] 10)
+  "_fBex1" :: "pttrn \<Rightarrow> 'a fset \<Rightarrow> bool \<Rightarrow> bool"  (\<open>(\<open>indent=3 notation=\<open>binder finite ?!\<close>\<close>?! (_/:_)./ _)\<close> [0, 0, 10] 10)
 
 syntax
-  "_fBall"       :: "pttrn \<Rightarrow> 'a fset \<Rightarrow> bool \<Rightarrow> bool"      (\<open>(3\<forall>(_/|\<in>|_)./ _)\<close> [0, 0, 10] 10)
-  "_fBex"        :: "pttrn \<Rightarrow> 'a fset \<Rightarrow> bool \<Rightarrow> bool"      (\<open>(3\<exists>(_/|\<in>|_)./ _)\<close> [0, 0, 10] 10)
+  "_fBall" :: "pttrn \<Rightarrow> 'a fset \<Rightarrow> bool \<Rightarrow> bool"  (\<open>(\<open>indent=3 notation=\<open>binder finite \<forall>\<close>\<close>\<forall>(_/|\<in>|_)./ _)\<close> [0, 0, 10] 10)
+  "_fBex"  :: "pttrn \<Rightarrow> 'a fset \<Rightarrow> bool \<Rightarrow> bool"  (\<open>(\<open>indent=3 notation=\<open>binder finite \<exists>\<close>\<close>\<exists>(_/|\<in>|_)./ _)\<close> [0, 0, 10] 10)
+  "_fBnex" :: "pttrn \<Rightarrow> 'a fset \<Rightarrow> bool \<Rightarrow> bool"  (\<open>(\<open>indent=3 notation=\<open>binder finite \<nexists>\<close>\<close>\<nexists>(_/|\<in>|_)./ _)\<close> [0, 0, 10] 10)
+  "_fBex1" :: "pttrn \<Rightarrow> 'a fset \<Rightarrow> bool \<Rightarrow> bool"  (\<open>(\<open>indent=3 notation=\<open>binder finite \<exists>!\<close>\<close>\<exists>!(_/|\<in>|_)./ _)\<close> [0, 0, 10] 10)
 
 syntax_consts
-  "_fBall" \<rightleftharpoons> FSet.Ball and
-  "_fBex" \<rightleftharpoons> FSet.Bex
+  "_fBall" "_fBnex" \<rightleftharpoons> fBall and
+  "_fBex" \<rightleftharpoons> fBex and
+  "_fBex1" \<rightleftharpoons> Ex1
 
 translations
   "\<forall>x|\<in>|A. P" \<rightleftharpoons> "CONST FSet.Ball A (\<lambda>x. P)"
   "\<exists>x|\<in>|A. P" \<rightleftharpoons> "CONST FSet.Bex A (\<lambda>x. P)"
+  "\<nexists>x|\<in>|A. P" \<rightleftharpoons> "CONST fBall A (\<lambda>x. \<not> P)"
+  "\<exists>!x|\<in>|A. P" \<rightharpoonup> "\<exists>!x. x |\<in>| A \<and> P"
 
 print_translation \<open>
  [Syntax_Trans.preserve_binder_abs2_tr' \<^const_syntax>\<open>fBall\<close> \<^syntax_const>\<open>_fBall\<close>,
   Syntax_Trans.preserve_binder_abs2_tr' \<^const_syntax>\<open>fBex\<close> \<^syntax_const>\<open>_fBex\<close>]
 \<close> \<comment> \<open>to avoid eta-contraction of body\<close>
 
+syntax
+  "_setlessfAll" :: "[idt, 'a, bool] \<Rightarrow> bool"   (\<open>(\<open>indent=3 notation=\<open>binder finite \<forall>\<close>\<close>\<forall>_|\<subset>|_./ _)\<close>  [0, 0, 10] 10)
+  "_setlessfEx"  :: "[idt, 'a, bool] \<Rightarrow> bool"   (\<open>(\<open>indent=3 notation=\<open>binder finite \<exists>\<close>\<close>\<exists>_|\<subset>|_./ _)\<close>  [0, 0, 10] 10)
+  "_setlefAll"   :: "[idt, 'a, bool] \<Rightarrow> bool"   (\<open>(\<open>indent=3 notation=\<open>binder finite \<forall>\<close>\<close>\<forall>_|\<subseteq>|_./ _)\<close> [0, 0, 10] 10)
+  "_setlefEx"    :: "[idt, 'a, bool] \<Rightarrow> bool"   (\<open>(\<open>indent=3 notation=\<open>binder finite \<exists>\<close>\<close>\<exists>_|\<subseteq>|_./ _)\<close> [0, 0, 10] 10)
+
+syntax_consts
+  "_setlessfAll" "_setlefAll" \<rightleftharpoons> All and
+  "_setlessfEx" "_setlefEx" \<rightleftharpoons> Ex
+
+translations
+ "\<forall>A|\<subset>|B. P" \<rightharpoonup> "\<forall>A. A |\<subset>| B \<longrightarrow> P"
+ "\<exists>A|\<subset>|B. P" \<rightharpoonup> "\<exists>A. A |\<subset>| B \<and> P"
+ "\<forall>A|\<subseteq>|B. P" \<rightharpoonup> "\<forall>A. A |\<subseteq>| B \<longrightarrow> P"
+ "\<exists>A|\<subseteq>|B. P" \<rightharpoonup> "\<exists>A. A |\<subseteq>| B \<and> P"
+
+
 context includes lifting_syntax
 begin
 
diff -r 28ef01901650 -r 92768949a923 src/HOL/Library/Landau_Symbols.thy
--- a/src/HOL/Library/Landau_Symbols.thy	Wed Oct 02 18:32:36 2024 +0200
+++ b/src/HOL/Library/Landau_Symbols.thy	Thu Oct 03 13:01:31 2024 +0200
@@ -1741,7 +1741,7 @@
 abbreviation (input) asymp_equiv_at_top where
   "asymp_equiv_at_top f g \<equiv> f \<sim>[at_top] g"
 
-bundle asymp_equiv_notation
+bundle asymp_equiv_syntax
 begin
 notation asymp_equiv_at_top (infix \<open>\<sim>\<close> 50)
 end
diff -r 28ef01901650 -r 92768949a923 src/HOL/Library/Multiset.thy
--- a/src/HOL/Library/Multiset.thy	Wed Oct 02 18:32:36 2024 +0200
+++ b/src/HOL/Library/Multiset.thy	Thu Oct 03 13:01:31 2024 +0200
@@ -92,9 +92,7 @@
 by (rule add_mset_in_multiset)
 
 syntax
-  "_multiset" :: "args \<Rightarrow> 'a multiset"    (\<open>{#(\<open>notation=\<open>mixfix multiset enumeration\<close>\<close>_)#}\<close>)
-syntax_consts
-  add_mset
+  "_multiset" :: "args \<Rightarrow> 'a multiset"  (\<open>(\<open>indent=2 notation=\<open>mixfix multiset enumeration\<close>\<close>{#_#})\<close>)
 translations
   "{#x, xs#}" == "CONST add_mset x {#xs#}"
   "{#x#}" == "CONST add_mset x {#}"
diff -r 28ef01901650 -r 92768949a923 src/HOL/List.thy
--- a/src/HOL/List.thy	Wed Oct 02 18:32:36 2024 +0200
+++ b/src/HOL/List.thy	Thu Oct 03 13:01:31 2024 +0200
@@ -46,12 +46,16 @@
 text \<open>List enumeration\<close>
 
 syntax
-  "_list" :: "args => 'a list"    (\<open>[(\<open>notation=\<open>mixfix list enumeration\<close>\<close>_)]\<close>)
-syntax_consts
-  Cons
+  "_list" :: "args \<Rightarrow> 'a list"  (\<open>(\<open>indent=1 notation=\<open>mixfix list enumeration\<close>\<close>[_])\<close>)
 translations
-  "[x, xs]" == "x#[xs]"
-  "[x]" == "x#[]"
+  "[x, xs]" \<rightleftharpoons> "x#[xs]"
+  "[x]" \<rightleftharpoons> "x#[]"
+
+bundle no_list_syntax
+begin
+no_syntax
+  "_list" :: "args \<Rightarrow> 'a list"  (\<open>(\<open>indent=1 notation=\<open>mixfix list enumeration\<close>\<close>[_])\<close>)
+end
 
 
 subsection \<open>Basic list processing functions\<close>
@@ -137,9 +141,6 @@
   "_lupdbinds" :: "[lupdbind, lupdbinds] => lupdbinds"    (\<open>_,/ _\<close>)
   "_LUpdate" :: "['a, lupdbinds] => 'a"    (\<open>_/[(_)]\<close> [1000,0] 900)
 
-syntax_consts
-  list_update
-
 translations
   "_LUpdate xs (_lupdbinds b bs)" == "_LUpdate (_LUpdate xs b) bs"
   "xs[i:=x]" == "CONST list_update xs i x"
@@ -456,6 +457,13 @@
 syntax (ASCII)
   "_lc_gen" :: "'a \<Rightarrow> 'a list \<Rightarrow> lc_qual"  (\<open>_ <- _\<close>)
 
+bundle no_listcompr_syntax
+begin
+no_syntax
+  "_listcompr" :: "'a \<Rightarrow> lc_qual \<Rightarrow> lc_quals \<Rightarrow> 'a list"  (\<open>[_ . __\<close>)
+  "_lc_end" :: "lc_quals" (\<open>]\<close>)
+end
+
 parse_translation \<open>
 let
   val NilC = Syntax.const \<^const_syntax>\<open>Nil\<close>;
diff -r 28ef01901650 -r 92768949a923 src/HOL/Metis_Examples/Message.thy
--- a/src/HOL/Metis_Examples/Message.thy	Wed Oct 02 18:32:36 2024 +0200
+++ b/src/HOL/Metis_Examples/Message.thy	Thu Oct 03 13:01:31 2024 +0200
@@ -50,8 +50,6 @@
 text\<open>Concrete syntax: messages appear as \<open>\<lbrace>A,B,NA\<rbrace>\<close>, etc...\<close>
 syntax
   "_MTuple" :: "['a, args] \<Rightarrow> 'a * 'b"  (\<open>(\<open>indent=2 notation=\<open>mixfix message tuple\<close>\<close>\<lbrace>_,/ _\<rbrace>)\<close>)
-syntax_consts
-  MPair
 translations
   "\<lbrace>x, y, z\<rbrace>" \<rightleftharpoons> "\<lbrace>x, \<lbrace>y, z\<rbrace>\<rbrace>"
   "\<lbrace>x, y\<rbrace>" \<rightleftharpoons> "CONST MPair x y"
diff -r 28ef01901650 -r 92768949a923 src/HOL/Product_Type.thy
--- a/src/HOL/Product_Type.thy	Wed Oct 02 18:32:36 2024 +0200
+++ b/src/HOL/Product_Type.thy	Thu Oct 03 13:01:31 2024 +0200
@@ -294,7 +294,6 @@
   "_patterns"   :: "pttrn \<Rightarrow> patterns \<Rightarrow> patterns"      (\<open>_,/ _\<close>)
   "_unit"       :: pttrn                                (\<open>'(')\<close>)
 syntax_consts
-  Pair and
   "_pattern" "_patterns" \<rightleftharpoons> case_prod and
   "_unit" \<rightleftharpoons> case_unit
 translations
@@ -804,10 +803,8 @@
 
 bundle state_combinator_syntax
 begin
-
 notation fcomp (infixl \<open>\<circ>>\<close> 60)
 notation scomp (infixl \<open>\<circ>\<rightarrow>\<close> 60)
-
 end
 
 context
@@ -1000,15 +997,19 @@
 definition Sigma :: "'a set \<Rightarrow> ('a \<Rightarrow> 'b set) \<Rightarrow> ('a \<times> 'b) set"
   where "Sigma A B \<equiv> \<Union>x\<in>A. \<Union>y\<in>B x. {Pair x y}"
 
-abbreviation Times :: "'a set \<Rightarrow> 'b set \<Rightarrow> ('a \<times> 'b) set"  (infixr \<open>\<times>\<close> 80)
+context
+begin
+qualified abbreviation Times :: "'a set \<Rightarrow> 'b set \<Rightarrow> ('a \<times> 'b) set"  (infixr \<open>\<times>\<close> 80)
   where "A \<times> B \<equiv> Sigma A (\<lambda>_. B)"
+end
 
-hide_const (open) Times
-
-bundle no_Set_Product_syntax begin
+bundle no_Set_Product_syntax
+begin
 no_notation Product_Type.Times (infixr \<open>\<times>\<close> 80)
 end
-bundle Set_Product_syntax begin
+
+bundle Set_Product_syntax
+begin
 notation Product_Type.Times (infixr \<open>\<times>\<close> 80)
 end
 
diff -r 28ef01901650 -r 92768949a923 src/HOL/Prolog/Test.thy
--- a/src/HOL/Prolog/Test.thy	Wed Oct 02 18:32:36 2024 +0200
+++ b/src/HOL/Prolog/Test.thy	Thu Oct 03 13:01:31 2024 +0200
@@ -19,9 +19,7 @@
 text \<open>List enumeration\<close>
 
 syntax
-  "_list" :: "args => 'a list"    (\<open>[(\<open>notation=\<open>mixfix list enumeration\<close>\<close>_)]\<close>)
-syntax_consts
-  Cons
+  "_list" :: "args => 'a list"  (\<open>(\<open>indent=1 notation=\<open>mixfix list enumeration\<close>\<close>[_])\<close>)
 translations
   "[x, xs]" == "x#[xs]"
   "[x]" == "x#[]"
diff -r 28ef01901650 -r 92768949a923 src/HOL/Quotient_Examples/Lift_FSet.thy
--- a/src/HOL/Quotient_Examples/Lift_FSet.thy	Wed Oct 02 18:32:36 2024 +0200
+++ b/src/HOL/Quotient_Examples/Lift_FSet.thy	Thu Oct 03 13:01:31 2024 +0200
@@ -96,9 +96,7 @@
 end
 
 syntax
-  "_fset" :: "args => 'a fset"  (\<open>{|(\<open>notation=\<open>mixfix finite set enumeration\<close>\<close>_)|}\<close>)
-syntax_consts
-  fcons
+  "_fset" :: "args => 'a fset"  (\<open>(\<open>indent=2 notation=\<open>mixfix finite set enumeration\<close>\<close>{|_|})\<close>)
 translations
   "{|x, xs|}" == "CONST fcons x {|xs|}"
   "{|x|}"     == "CONST fcons x {||}"
diff -r 28ef01901650 -r 92768949a923 src/HOL/Quotient_Examples/Quotient_FSet.thy
--- a/src/HOL/Quotient_Examples/Quotient_FSet.thy	Wed Oct 02 18:32:36 2024 +0200
+++ b/src/HOL/Quotient_Examples/Quotient_FSet.thy	Thu Oct 03 13:01:31 2024 +0200
@@ -289,9 +289,7 @@
   is "Cons" by auto
 
 syntax
-  "_fset" :: "args => 'a fset"  (\<open>{|(\<open>notation=\<open>mixfix finite set enumeration\<close>\<close>_)|}\<close>)
-syntax_consts
-  insert_fset
+  "_fset" :: "args => 'a fset"  (\<open>(\<open>indent=2 notation=\<open>mixfix finite set enumeration\<close>\<close>{|_|})\<close>)
 translations
   "{|x, xs|}" == "CONST insert_fset x {|xs|}"
   "{|x|}"     == "CONST insert_fset x {||}"
diff -r 28ef01901650 -r 92768949a923 src/HOL/Real_Asymp/Multiseries_Expansion.thy
--- a/src/HOL/Real_Asymp/Multiseries_Expansion.thy	Wed Oct 02 18:32:36 2024 +0200
+++ b/src/HOL/Real_Asymp/Multiseries_Expansion.thy	Thu Oct 03 13:01:31 2024 +0200
@@ -1716,7 +1716,7 @@
   shows   "f \<sim>[at_top] eval_monom (dominant_term_ms_aux xs) basis" (is ?thesis1)
     and   "eventually (\<lambda>x. sgn (f x) = sgn (fst (dominant_term_ms_aux xs))) at_top" (is ?thesis2)
 proof -
-  include asymp_equiv_notation
+  include asymp_equiv_syntax
   from xs(2,1) obtain xs' C b e basis' where xs':
     "trimmed C" "xs = MSLCons (C, e) xs'" "basis = b # basis'"
     "is_expansion_aux xs' (\<lambda>x. f x - eval C x * b x powr e) (b # basis')"
diff -r 28ef01901650 -r 92768949a923 src/HOL/Real_Asymp/Real_Asymp_Examples.thy
--- a/src/HOL/Real_Asymp/Real_Asymp_Examples.thy	Wed Oct 02 18:32:36 2024 +0200
+++ b/src/HOL/Real_Asymp/Real_Asymp_Examples.thy	Thu Oct 03 13:01:31 2024 +0200
@@ -4,7 +4,7 @@
 begin
 
 context
-  includes asymp_equiv_notation
+  includes asymp_equiv_syntax
 begin
 
 subsection \<open>Dominik Gruntz's examples\<close>
diff -r 28ef01901650 -r 92768949a923 src/HOL/SET_Protocol/Message_SET.thy
--- a/src/HOL/SET_Protocol/Message_SET.thy	Wed Oct 02 18:32:36 2024 +0200
+++ b/src/HOL/SET_Protocol/Message_SET.thy	Thu Oct 03 13:01:31 2024 +0200
@@ -70,8 +70,6 @@
 (*Concrete syntax: messages appear as \<open>\<lbrace>A,B,NA\<rbrace>\<close>, etc...*)
 syntax
   "_MTuple" :: "['a, args] \<Rightarrow> 'a * 'b"  (\<open>(\<open>indent=2 notation=\<open>mixfix message tuple\<close>\<close>\<lbrace>_,/ _\<rbrace>)\<close>)
-syntax_consts
-  MPair
 translations
   "\<lbrace>x, y, z\<rbrace>" \<rightleftharpoons> "\<lbrace>x, \<lbrace>y, z\<rbrace>\<rbrace>"
   "\<lbrace>x, y\<rbrace>" \<rightleftharpoons> "CONST MPair x y"
diff -r 28ef01901650 -r 92768949a923 src/HOL/Set.thy
--- a/src/HOL/Set.thy	Wed Oct 02 18:32:36 2024 +0200
+++ b/src/HOL/Set.thy	Thu Oct 03 13:01:31 2024 +0200
@@ -39,18 +39,14 @@
 text \<open>Set comprehensions\<close>
 
 syntax
-  "_Coll" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a set"    (\<open>(\<open>indent=1 notation=\<open>mixfix Collect\<close>\<close>{_./ _})\<close>)
-syntax_consts
-  "_Coll" \<rightleftharpoons> Collect
+  "_Coll" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a set"    (\<open>(\<open>indent=1 notation=\<open>mixfix set comprehension\<close>\<close>{_./ _})\<close>)
 translations
   "{x. P}" \<rightleftharpoons> "CONST Collect (\<lambda>x. P)"
 
 syntax (ASCII)
-  "_Collect" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> bool \<Rightarrow> 'a set"  (\<open>(\<open>indent=1 notation=\<open>mixfix Collect\<close>\<close>{(_/: _)./ _})\<close>)
+  "_Collect" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> bool \<Rightarrow> 'a set"  (\<open>(\<open>indent=1 notation=\<open>mixfix set comprehension\<close>\<close>{(_/: _)./ _})\<close>)
 syntax
-  "_Collect" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> bool \<Rightarrow> 'a set"  (\<open>(\<open>indent=1 notation=\<open>mixfix Collect\<close>\<close>{(_/ \<in> _)./ _})\<close>)
-syntax_consts
-  "_Collect" \<rightleftharpoons> Collect
+  "_Collect" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> bool \<Rightarrow> 'a set"  (\<open>(\<open>indent=1 notation=\<open>mixfix set comprehension\<close>\<close>{(_/ \<in> _)./ _})\<close>)
 translations
   "{p:A. P}" \<rightharpoonup> "CONST Collect (\<lambda>p. p \<in> A \<and> P)"
 
@@ -144,9 +140,7 @@
   where insert_compr: "insert a B = {x. x = a \<or> x \<in> B}"
 
 syntax
-  "_Finset" :: "args \<Rightarrow> 'a set"    (\<open>{(\<open>notation=\<open>mixfix set enumeration\<close>\<close>_)}\<close>)
-syntax_consts
-  insert
+  "_Finset" :: "args \<Rightarrow> 'a set"  (\<open>(\<open>indent=1 notation=\<open>mixfix set enumeration\<close>\<close>{_})\<close>)
 translations
   "{x, xs}" \<rightleftharpoons> "CONST insert x {xs}"
   "{x}" \<rightleftharpoons> "CONST insert x {}"
diff -r 28ef01901650 -r 92768949a923 src/HOL/Tools/Lifting/lifting_setup.ML
--- a/src/HOL/Tools/Lifting/lifting_setup.ML	Wed Oct 02 18:32:36 2024 +0200
+++ b/src/HOL/Tools/Lifting/lifting_setup.ML	Thu Oct 03 13:01:31 2024 +0200
@@ -245,7 +245,7 @@
     lthy
     |> Local_Theory.declaration {syntax = false, pervasive = true, pos = \<^here>}
         (fn phi => Lifting_Info.init_restore_data bundle_name (phi_qinfo phi))
-    |> Bundle.bundle ((binding, [restore_lifting_att])) []
+    |> Bundle.bundle {open_bundle = false} ((binding, [restore_lifting_att])) []
     |> pair binding
   end
 
diff -r 28ef01901650 -r 92768949a923 src/HOL/Transfer.thy
--- a/src/HOL/Transfer.thy	Wed Oct 02 18:32:36 2024 +0200
+++ b/src/HOL/Transfer.thy	Thu Oct 03 13:01:31 2024 +0200
@@ -13,8 +13,8 @@
 
 bundle lifting_syntax
 begin
-  notation rel_fun  (infixr \<open>===>\<close> 55)
-  notation map_fun  (infixr \<open>--->\<close> 55)
+notation rel_fun  (infixr \<open>===>\<close> 55)
+notation map_fun  (infixr \<open>--->\<close> 55)
 end
 
 context includes lifting_syntax
diff -r 28ef01901650 -r 92768949a923 src/HOL/Transitive_Closure.thy
--- a/src/HOL/Transitive_Closure.thy	Wed Oct 02 18:32:36 2024 +0200
+++ b/src/HOL/Transitive_Closure.thy	Thu Oct 03 13:01:31 2024 +0200
@@ -64,6 +64,36 @@
   tranclp  (\<open>(\<open>notation=\<open>postfix ++\<close>\<close>_^++)\<close> [1000] 1000) and
   reflclp  (\<open>(\<open>notation=\<open>postfix ==\<close>\<close>_^==)\<close> [1000] 1000)
 
+bundle no_rtrancl_syntax
+begin
+no_notation
+  rtrancl  (\<open>(\<open>notation=\<open>postfix *\<close>\<close>_\<^sup>*)\<close> [1000] 999) and
+  rtranclp  (\<open>(\<open>notation=\<open>postfix **\<close>\<close>_\<^sup>*\<^sup>*)\<close> [1000] 1000)
+no_notation (ASCII)
+  rtrancl  (\<open>(\<open>notation=\<open>postfix *\<close>\<close>_^*)\<close> [1000] 999) and
+  rtranclp  (\<open>(\<open>notation=\<open>postfix **\<close>\<close>_^**)\<close> [1000] 1000)
+end
+
+bundle no_trancl_syntax
+begin
+no_notation
+  trancl  (\<open>(\<open>notation=\<open>postfix +\<close>\<close>_\<^sup>+)\<close> [1000] 999) and
+  tranclp  (\<open>(\<open>notation=\<open>postfix ++\<close>\<close>_\<^sup>+\<^sup>+)\<close> [1000] 1000)
+no_notation (ASCII)
+  trancl  (\<open>(\<open>notation=\<open>postfix +\<close>\<close>_^+)\<close> [1000] 999) and
+  tranclp  (\<open>(\<open>notation=\<open>postfix ++\<close>\<close>_^++)\<close> [1000] 1000)
+end
+
+bundle no_reflcl_syntax
+begin
+no_notation
+  reflcl  (\<open>(\<open>notation=\<open>postfix =\<close>\<close>_\<^sup>=)\<close> [1000] 999) and
+  reflclp  (\<open>(\<open>notation=\<open>postfix ==\<close>\<close>_\<^sup>=\<^sup>=)\<close> [1000] 1000)
+no_notation (ASCII)
+  reflcl  (\<open>(\<open>notation=\<open>postfix =\<close>\<close>_^=)\<close> [1000] 999) and
+  reflclp  (\<open>(\<open>notation=\<open>postfix ==\<close>\<close>_^==)\<close> [1000] 1000)
+end
+
 
 subsection \<open>Reflexive closure\<close>
 
diff -r 28ef01901650 -r 92768949a923 src/HOL/ex/Code_Lazy_Demo.thy
--- a/src/HOL/ex/Code_Lazy_Demo.thy	Wed Oct 02 18:32:36 2024 +0200
+++ b/src/HOL/ex/Code_Lazy_Demo.thy	Thu Oct 03 13:01:31 2024 +0200
@@ -40,9 +40,7 @@
   | LCons (lhd: 'a) (ltl: "'a llist") (infixr \<open>###\<close> 65)
 
 syntax
-  "_llist" :: "args => 'a list"    (\<open>\<^bold>\<lbrakk>(\<open>notation=\<open>mixfix lazy list enumeration\<close>\<close>_)\<^bold>\<rbrakk>\<close>)
-syntax_consts
-  LCons
+  "_llist" :: "args => 'a list"  (\<open>(\<open>indent=1 notation=\<open>mixfix lazy list enumeration\<close>\<close>\<^bold>\<lbrakk>_\<^bold>\<rbrakk>)\<close>)
 translations
   "\<^bold>\<lbrakk>x, xs\<^bold>\<rbrakk>" == "x###\<^bold>\<lbrakk>xs\<^bold>\<rbrakk>"
   "\<^bold>\<lbrakk>x\<^bold>\<rbrakk>" == "x###\<^bold>\<lbrakk>\<^bold>\<rbrakk>"
diff -r 28ef01901650 -r 92768949a923 src/Pure/Isar/bundle.ML
--- a/src/Pure/Isar/bundle.ML	Wed Oct 02 18:32:36 2024 +0200
+++ b/src/Pure/Isar/bundle.ML	Thu Oct 03 13:01:31 2024 +0200
@@ -13,11 +13,6 @@
   val read: Proof.context -> xstring * Position.T -> Attrib.thms
   val extern: Proof.context -> string -> xstring
   val print_bundles: bool -> Proof.context -> unit
-  val bundle: binding * Attrib.thms ->
-    (binding * typ option * mixfix) list -> local_theory -> local_theory
-  val bundle_cmd: binding * (Facts.ref * Token.src list) list ->
-    (binding * string option * mixfix) list -> local_theory -> local_theory
-  val init: binding -> theory -> local_theory
   val unbundle: name list -> local_theory -> local_theory
   val unbundle_cmd: (xstring * Position.T) list -> local_theory -> local_theory
   val includes: name list -> Proof.context -> Proof.context
@@ -26,6 +21,11 @@
   val include_cmd: (xstring * Position.T) list -> Proof.state -> Proof.state
   val including: name list -> Proof.state -> Proof.state
   val including_cmd: (xstring * Position.T) list -> Proof.state -> Proof.state
+  val bundle: {open_bundle: bool} -> binding * Attrib.thms ->
+    (binding * typ option * mixfix) list -> local_theory -> local_theory
+  val bundle_cmd: {open_bundle: bool} -> binding * (Facts.ref * Token.src list) list ->
+    (binding * string option * mixfix) list -> local_theory -> local_theory
+  val init: {open_bundle: bool} -> binding -> theory -> local_theory
 end;
 
 structure Bundle: BUNDLE =
@@ -53,6 +53,7 @@
 
 fun check ctxt = #1 o Name_Space.check (Context.Proof ctxt) (get_all ctxt);
 
+val get_global = Name_Space.get o get_all_generic o Context.Theory;
 val get = Name_Space.get o get_all_generic o Context.Proof;
 
 fun read ctxt = get ctxt o check ctxt;
@@ -60,6 +61,19 @@
 fun extern ctxt = Name_Space.extern ctxt (Name_Space.space_of_table (get_all ctxt));
 
 
+(* context and morphisms *)
+
+val trim_context_bundle =
+  map (fn (fact, atts) => (map Thm.trim_context fact, (map o map) Token.trim_context atts));
+
+fun transfer_bundle thy =
+  map (fn (fact, atts) => (map (Thm.transfer thy) fact, (map o map) (Token.transfer thy) atts));
+
+fun transform_bundle phi =
+  map (fn (fact, atts) => (Morphism.fact phi fact, (map o map) (Token.transform phi) atts));
+
+
+
 (* target -- bundle under construction *)
 
 fun the_target thy =
@@ -93,18 +107,51 @@
 
 
 
-(** define bundle **)
+(** open bundles **)
+
+fun apply_bundle loc bundle ctxt =
+  let val notes = if loc then Local_Theory.notes else Attrib.local_notes "" in
+    ctxt
+    |> Context_Position.set_visible false
+    |> notes [(Binding.empty_atts, bundle)] |> snd
+    |> Context_Position.restore_visible ctxt
+  end;
 
-(* context and morphisms *)
+local
+
+fun gen_unbundle loc prep args ctxt =
+  let
+    val thy = Proof_Context.theory_of ctxt;
+    val bundle = maps (prep ctxt) args |> transfer_bundle thy;
+  in apply_bundle loc bundle ctxt end;
+
+fun gen_includes prep = gen_unbundle false prep;
+
+fun gen_include prep bs =
+  Proof.assert_forward #> Proof.map_context (gen_includes prep bs) #> Proof.reset_facts;
 
-val trim_context_bundle =
-  map (fn (fact, atts) => (map Thm.trim_context fact, (map o map) Token.trim_context atts));
+fun gen_including prep bs =
+  Proof.assert_backward #> Proof.map_context (gen_includes prep bs);
+
+in
+
+val unbundle = gen_unbundle true get;
+val unbundle_cmd = gen_unbundle true read;
+
+val includes = gen_includes get;
+val includes_cmd = gen_includes read;
 
-fun transfer_bundle thy =
-  map (fn (fact, atts) => (map (Thm.transfer thy) fact, (map o map) (Token.transfer thy) atts));
+val include_ = gen_include get;
+val include_cmd = gen_include read;
+
+val including = gen_including get;
+val including_cmd = gen_including read;
 
-fun transform_bundle phi =
-  map (fn (fact, atts) => (Morphism.fact phi fact, (map o map) (Token.transform phi) atts));
+end;
+
+
+
+(** define bundle **)
 
 fun define_bundle (b, bundle) context =
   let
@@ -118,7 +165,7 @@
 
 local
 
-fun gen_bundle prep_fact prep_att add_fixes (binding, raw_bundle) raw_fixes lthy =
+fun gen_bundle prep_fact prep_att add_fixes {open_bundle} (binding, raw_bundle) raw_fixes lthy =
   let
     val (_, ctxt') = add_fixes raw_fixes lthy;
     val bundle0 = raw_bundle
@@ -133,6 +180,7 @@
       (fn phi => fn context =>
         let val psi = Morphism.set_trim_context'' context phi
         in #2 (define_bundle (Morphism.binding psi binding, transform_bundle psi bundle) context) end)
+    |> open_bundle ? apply_bundle true bundle
   end;
 
 in
@@ -149,22 +197,29 @@
 
 fun bad_operation _ = error "Not possible in bundle target";
 
-fun conclude invisible binding =
+fun conclude {open_bundle, invisible} binding =
   Local_Theory.background_theory_result (fn thy =>
-    thy
-    |> invisible ? Context_Position.set_visible_global false
-    |> Context.Theory
-    |> define_bundle (binding, the_target thy)
-    ||> (Context.the_theory
-      #> invisible ? Context_Position.restore_visible_global thy
-      #> reset_target));
+    let
+      val (name, thy') = thy
+        |> invisible ? Context_Position.set_visible_global false
+        |> Context.Theory
+        |> define_bundle (binding, the_target thy)
+        ||> Context.the_theory;
+      val bundle = get_global thy' name;
+      val thy'' = thy'
+        |> open_bundle ?
+          (Context_Position.set_visible_global false #>
+            Attrib.global_notes "" [(Binding.empty_atts, bundle)] #> snd)
+        |> Context_Position.restore_visible_global thy
+        |> reset_target;
+    in (name, thy'') end);
 
 fun pretty binding lthy =
   let
     val bundle = the_target (Proof_Context.theory_of lthy);
     val (name, lthy') = lthy
       |> Local_Theory.raw_theory (Context_Position.set_visible_global false)
-      |> conclude true binding;
+      |> conclude {open_bundle = false, invisible = true} binding;
     val thy_ctxt' = Proof_Context.init_global (Proof_Context.theory_of lthy');
     val markup_name =
       Name_Space.markup_extern thy_ctxt' (Name_Space.space_of_table (get_all thy_ctxt')) name;
@@ -189,12 +244,12 @@
 
 in
 
-fun init binding thy =
+fun init {open_bundle} binding thy =
   thy
   |> Local_Theory.init
      {background_naming = Sign.naming_of thy,
       setup = set_target [] #> Proof_Context.init_global,
-      conclude = conclude false binding #> #2}
+      conclude = conclude {open_bundle = open_bundle, invisible = false} binding #> #2}
      {define = bad_operation,
       notes = bundle_notes,
       abbrev = bad_operation,
@@ -205,47 +260,4 @@
 
 end;
 
-
-
-(** activate bundles **)
-
-local
-
-fun gen_activate notes prep_bundle args ctxt =
-  let
-    val thy = Proof_Context.theory_of ctxt;
-    val decls = maps (prep_bundle ctxt) args |> transfer_bundle thy;
-  in
-    ctxt
-    |> Context_Position.set_visible false
-    |> notes [(Binding.empty_atts, decls)] |> #2
-    |> Context_Position.restore_visible ctxt
-  end;
-
-fun gen_unbundle prep_bundle = gen_activate Local_Theory.notes prep_bundle;
-
-fun gen_includes prep_bundle = gen_activate (Attrib.local_notes "") prep_bundle;
-
-fun gen_include prep_bundle bs =
-  Proof.assert_forward #> Proof.map_context (gen_includes prep_bundle bs) #> Proof.reset_facts;
-
-fun gen_including prep_bundle bs =
-  Proof.assert_backward #> Proof.map_context (gen_includes prep_bundle bs)
-
-in
-
-val unbundle = gen_unbundle get;
-val unbundle_cmd = gen_unbundle read;
-
-val includes = gen_includes get;
-val includes_cmd = gen_includes read;
-
-val include_ = gen_include get;
-val include_cmd = gen_include read;
-
-val including = gen_including get;
-val including_cmd = gen_including read;
-
 end;
-
-end;
diff -r 28ef01901650 -r 92768949a923 src/Pure/Pure.thy
--- a/src/Pure/Pure.thy	Wed Oct 02 18:32:36 2024 +0200
+++ b/src/Pure/Pure.thy	Thu Oct 03 13:01:31 2024 +0200
@@ -37,7 +37,7 @@
     "declaration" "syntax_declaration"
     "parse_ast_translation" "parse_translation" "print_translation"
     "typed_print_translation" "print_ast_translation" "oracle" :: thy_decl % "ML"
-  and "bundle" :: thy_decl_block
+  and "bundle" "open_bundle" :: thy_decl_block
   and "unbundle" :: thy_decl
   and "include" "including" :: prf_decl
   and "print_bundles" :: diag
@@ -637,26 +637,34 @@
 ML \<open>
 local
 
+fun bundle_cmd open_bundle =
+  (Parse.binding --| \<^keyword>\<open>=\<close>) -- Parse.thms1 -- Parse.for_fixes
+    >> (uncurry (Bundle.bundle_cmd {open_bundle = open_bundle}));
+
+fun bundle_begin open_bundle =
+  Parse.binding --| Parse.begin >> Bundle.init {open_bundle = open_bundle};
+
 val _ =
   Outer_Syntax.maybe_begin_local_theory \<^command_keyword>\<open>bundle\<close>
-    "define bundle of declarations"
-    ((Parse.binding --| \<^keyword>\<open>=\<close>) -- Parse.thms1 -- Parse.for_fixes
-      >> (uncurry Bundle.bundle_cmd))
-    (Parse.binding --| Parse.begin >> Bundle.init);
+    "define bundle of declarations" (bundle_cmd false) (bundle_begin false);
+
+val _ =
+  Outer_Syntax.maybe_begin_local_theory \<^command_keyword>\<open>open_bundle\<close>
+    "define and open bundle of declarations" (bundle_cmd true) (bundle_begin true);
 
 val _ =
   Outer_Syntax.local_theory \<^command_keyword>\<open>unbundle\<close>
-    "activate declarations from bundle in local theory"
+    "open bundle in local theory"
     (Scan.repeat1 Parse.name_position >> Bundle.unbundle_cmd);
 
 val _ =
   Outer_Syntax.command \<^command_keyword>\<open>include\<close>
-    "activate declarations from bundle in proof body"
+    "open bundle in proof body"
     (Scan.repeat1 Parse.name_position >> (Toplevel.proof o Bundle.include_cmd));
 
 val _ =
   Outer_Syntax.command \<^command_keyword>\<open>including\<close>
-    "activate declarations from bundle in goal refinement"
+    "open bundle in goal refinement"
     (Scan.repeat1 Parse.name_position >> (Toplevel.proof o Bundle.including_cmd));
 
 val _ =
diff -r 28ef01901650 -r 92768949a923 src/ZF/Induct/Multiset.thy
--- a/src/ZF/Induct/Multiset.thy	Wed Oct 02 18:32:36 2024 +0200
+++ b/src/ZF/Induct/Multiset.thy	Thu Oct 03 13:01:31 2024 +0200
@@ -75,8 +75,6 @@
 
 syntax
   "_MColl" :: "[pttrn, i, o] \<Rightarrow> i" (\<open>(\<open>indent=1 notation=\<open>mixfix multiset comprehension\<close>\<close>{# _ \<in> _./ _#})\<close>)
-syntax_consts
-  MCollect
 translations
   "{#x \<in> M. P#}" == "CONST MCollect(M, \<lambda>x. P)"
 
diff -r 28ef01901650 -r 92768949a923 src/ZF/List.thy
--- a/src/ZF/List.thy	Wed Oct 02 18:32:36 2024 +0200
+++ b/src/ZF/List.thy	Thu Oct 03 13:01:31 2024 +0200
@@ -16,9 +16,7 @@
 notation Nil (\<open>[]\<close>)
 
 syntax
-  "_List" :: "is \<Rightarrow> i"  (\<open>[(\<open>notation=\<open>mixfix list enumeration\<close>\<close>_)]\<close>)
-syntax_consts
-  Cons
+  "_List" :: "is \<Rightarrow> i"  (\<open>(\<open>indent=1 notation=\<open>mixfix list enumeration\<close>\<close>[_])\<close>)
 translations
   "[x, xs]"     == "CONST Cons(x, [xs])"
   "[x]"         == "CONST Cons(x, [])"
diff -r 28ef01901650 -r 92768949a923 src/ZF/ZF_Base.thy
--- a/src/ZF/ZF_Base.thy	Wed Oct 02 18:32:36 2024 +0200
+++ b/src/ZF/ZF_Base.thy	Thu Oct 03 13:01:31 2024 +0200
@@ -56,8 +56,6 @@
 
 syntax
   "_Replace" :: "[pttrn, pttrn, i, o] \<Rightarrow> i"  (\<open>(\<open>indent=1 notation=\<open>mixfix relational replacement\<close>\<close>{_ ./ _ \<in> _, _})\<close>)
-syntax_consts
-  Replace
 translations
   "{y. x\<in>A, Q}" \<rightleftharpoons> "CONST Replace(A, \<lambda>x y. Q)"
 
@@ -69,8 +67,6 @@
 
 syntax
   "_RepFun" :: "[i, pttrn, i] \<Rightarrow> i"  (\<open>(\<open>indent=1 notation=\<open>mixfix functional replacement\<close>\<close>{_ ./ _ \<in> _})\<close> [51,0,51])
-syntax_consts
-  RepFun
 translations
   "{b. x\<in>A}" \<rightleftharpoons> "CONST RepFun(A, \<lambda>x. b)"
 
@@ -81,8 +77,6 @@
 
 syntax
   "_Collect" :: "[pttrn, i, o] \<Rightarrow> i"  (\<open>(\<open>indent=1 notation=\<open>mixfix set comprehension\<close>\<close>{_ \<in> _ ./ _})\<close>)
-syntax_consts
-  Collect
 translations
   "{x\<in>A. P}" \<rightleftharpoons> "CONST Collect(A, \<lambda>x. P)"
 
@@ -133,9 +127,7 @@
 syntax
   "" :: "i \<Rightarrow> is"  (\<open>_\<close>)
   "_Enum" :: "[i, is] \<Rightarrow> is"  (\<open>_,/ _\<close>)
-  "_Finset" :: "is \<Rightarrow> i"  (\<open>{(\<open>notation=\<open>mixfix set enumeration\<close>\<close>_)}\<close>)
-syntax_consts
-  cons
+  "_Finset" :: "is \<Rightarrow> i"  (\<open>(\<open>indent=1 notation=\<open>mixfix set enumeration\<close>\<close>{_})\<close>)
 translations
   "{x, xs}" == "CONST cons(x, {xs})"
   "{x}" == "CONST cons(x, 0)"
@@ -196,9 +188,7 @@
 syntax
   "" :: "i \<Rightarrow> tuple_args"  (\<open>_\<close>)
   "_Tuple_args" :: "[i, tuple_args] \<Rightarrow> tuple_args"  (\<open>_,/ _\<close>)
-  "_Tuple" :: "[i, tuple_args] \<Rightarrow> i"              (\<open>\<langle>(\<open>notation=\<open>mixfix tuple enumeration\<close>\<close>_,/ _)\<rangle>\<close>)
-syntax_consts
-  Pair
+  "_Tuple" :: "[i, tuple_args] \<Rightarrow> i"  (\<open>(\<open>indent=1 notation=\<open>mixfix tuple enumeration\<close>\<close>\<langle>_,/ _\<rangle>)\<close>)
 translations
   "\<langle>x, y, z\<rangle>"   == "\<langle>x, \<langle>y, z\<rangle>\<rangle>"
   "\<langle>x, y\<rangle>"      == "CONST Pair(x, y)"
diff -r 28ef01901650 -r 92768949a923 src/ZF/func.thy
--- a/src/ZF/func.thy	Wed Oct 02 18:32:36 2024 +0200
+++ b/src/ZF/func.thy	Thu Oct 03 13:01:31 2024 +0200
@@ -452,8 +452,6 @@
   ""            :: "updbind \<Rightarrow> updbinds"             (\<open>_\<close>)
   "_updbinds"   :: "[updbind, updbinds] \<Rightarrow> updbinds" (\<open>_,/ _\<close>)
   "_Update"     :: "[i, updbinds] \<Rightarrow> i"              (\<open>_/'((_)')\<close> [900,0] 900)
-syntax_consts
-  update
 translations
   "_Update (f, _updbinds(b,bs))"  == "_Update (_Update(f,b), bs)"
   "f(x:=y)"                       == "CONST update(f,x,y)"