# HG changeset patch
# User wenzelm
# Date 1729254009 -7200
# Node ID fc5066122e68f583a4d6b95792094e05b5598f1e
# Parent  ff2a637a449e9dec4f2d80f6692bdf9c45096ef3
more inner-syntax markup;

diff -r ff2a637a449e -r fc5066122e68 src/CCL/Set.thy
--- a/src/CCL/Set.thy	Fri Oct 18 11:44:05 2024 +0200
+++ b/src/CCL/Set.thy	Fri Oct 18 14:20:09 2024 +0200
@@ -19,6 +19,8 @@
 
 syntax
   "_Coll" :: "[idt, o] \<Rightarrow> 'a set"  (\<open>(\<open>indent=1 notation=\<open>mixfix Collect\<close>\<close>{_./ _})\<close>)
+syntax_consts
+  "_Coll" == Collect
 translations
   "{x. P}" == "CONST Collect(\<lambda>x. P)"
 
diff -r ff2a637a449e -r fc5066122e68 src/CCL/Term.thy
--- a/src/CCL/Term.thy	Fri Oct 18 11:44:05 2024 +0200
+++ b/src/CCL/Term.thy	Fri Oct 18 14:20:09 2024 +0200
@@ -51,6 +51,7 @@
 
 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" == 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"
@@ -72,6 +73,10 @@
     (\<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" == letrec and
+  "_letrec2" == letrec2 and
+  "_letrec3" == letrec3
 parse_translation \<open>
   let
     fun abs_tr t u = Syntax_Trans.abs_tr [t, u];
diff -r ff2a637a449e -r fc5066122e68 src/CCL/Type.thy
--- a/src/CCL/Type.thy	Fri Oct 18 11:44:05 2024 +0200
+++ b/src/CCL/Type.thy	Fri Oct 18 14:20:09 2024 +0200
@@ -14,6 +14,8 @@
 
 syntax
   "_Subtype" :: "[idt, 'a set, o] \<Rightarrow> 'a set"  (\<open>(\<open>indent=1 notation=\<open>mixfix Subtype\<close>\<close>{_: _ ./ _})\<close>)
+syntax_consts
+  "_Subtype" == Subtype
 translations
   "{x: A. B}" == "CONST Subtype(A, \<lambda>x. B)"
 
diff -r ff2a637a449e -r fc5066122e68 src/FOL/IFOL.thy
--- a/src/FOL/IFOL.thy	Fri Oct 18 11:44:05 2024 +0200
+++ b/src/FOL/IFOL.thy	Fri Oct 18 14:20:09 2024 +0200
@@ -747,6 +747,8 @@
   ""            :: \<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 expression\<close>\<close>let (_)/ in (_))\<close> 10)
+syntax_consts
+  "_Let" \<rightleftharpoons> 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 ff2a637a449e -r fc5066122e68 src/HOL/Analysis/Bochner_Integration.thy
--- a/src/HOL/Analysis/Bochner_Integration.thy	Fri Oct 18 11:44:05 2024 +0200
+++ b/src/HOL/Analysis/Bochner_Integration.thy	Fri Oct 18 14:20:09 2024 +0200
@@ -892,20 +892,16 @@
 syntax
   "_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
-
 translations
   "\<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>(\<open>indent=3 notation=\<open>mixfix LINT\<close>\<close>LINT (1_)/|(_)./ _)\<close> [0,110,60] 60)
-
 syntax_consts
   "_ascii_lebesgue_integral" == lebesgue_integral
-
 translations
   "LINT x|M. f" == "CONST lebesgue_integral M (\<lambda>x. f)"
 
diff -r ff2a637a449e -r fc5066122e68 src/HOL/Analysis/Interval_Integral.thy
--- a/src/HOL/Analysis/Interval_Integral.thy	Fri Oct 18 11:44:05 2024 +0200
+++ b/src/HOL/Analysis/Interval_Integral.thy	Fri Oct 18 14:20:09 2024 +0200
@@ -147,10 +147,8 @@
 syntax
   "_ascii_interval_lebesgue_integral" :: "pttrn \<Rightarrow> real \<Rightarrow> real \<Rightarrow> real measure \<Rightarrow> real \<Rightarrow> real"
   (\<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
-
 translations
   "LINT x=a..b|M. f" == "CONST interval_lebesgue_integral M a b (\<lambda>x. f)"
 
@@ -161,10 +159,8 @@
 syntax
   "_ascii_interval_lebesgue_borel_integral" :: "pttrn \<Rightarrow> real \<Rightarrow> real \<Rightarrow> real \<Rightarrow> real"
   (\<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
-
 translations
   "LBINT x=a..b. f" == "CONST interval_lebesgue_integral CONST lborel a b (\<lambda>x. f)"
 
@@ -1050,18 +1046,14 @@
 
 syntax "_complex_lebesgue_borel_integral" :: "pttrn \<Rightarrow> real \<Rightarrow> complex"
   (\<open>(\<open>indent=2 notation=\<open>binder CLBINT\<close>\<close>CLBINT _. _)\<close> [0,60] 60)
-
 syntax_consts
   "_complex_lebesgue_borel_integral" == complex_lebesgue_integral
-
 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>(\<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
-
 translations
   "CLBINT x:A. f" == "CONST complex_set_lebesgue_integral CONST lborel A (\<lambda>x. f)"
 
@@ -1076,10 +1068,8 @@
 syntax
   "_ascii_complex_interval_lebesgue_borel_integral" :: "pttrn \<Rightarrow> ereal \<Rightarrow> ereal \<Rightarrow> real \<Rightarrow> complex"
   (\<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
-
 translations
   "CLBINT x=a..b. f" == "CONST complex_interval_lebesgue_integral CONST lborel a b (\<lambda>x. f)"
 
diff -r ff2a637a449e -r fc5066122e68 src/HOL/Analysis/Nonnegative_Lebesgue_Integration.thy
--- a/src/HOL/Analysis/Nonnegative_Lebesgue_Integration.thy	Fri Oct 18 11:44:05 2024 +0200
+++ b/src/HOL/Analysis/Nonnegative_Lebesgue_Integration.thy	Fri Oct 18 14:20:09 2024 +0200
@@ -820,10 +820,8 @@
 
 syntax
   "_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
-
 translations
   "\<integral>\<^sup>+x. f \<partial>M" == "CONST nn_integral M (\<lambda>x. f)"
 
diff -r ff2a637a449e -r fc5066122e68 src/HOL/Analysis/Set_Integral.thy
--- a/src/HOL/Analysis/Set_Integral.thy	Fri Oct 18 11:44:05 2024 +0200
+++ b/src/HOL/Analysis/Set_Integral.thy	Fri Oct 18 14:20:09 2024 +0200
@@ -25,10 +25,8 @@
 syntax
   "_ascii_set_lebesgue_integral" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'a measure \<Rightarrow> real \<Rightarrow> real"
   (\<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
-
 translations
   "LINT x:A|M. f" == "CONST set_lebesgue_integral M A (\<lambda>x. f)"
 
@@ -621,10 +619,8 @@
 syntax
   "_ascii_complex_set_lebesgue_integral" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'a measure \<Rightarrow> real \<Rightarrow> real"
   (\<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
-
 translations
   "CLINT x:A|M. f" == "CONST complex_set_lebesgue_integral M A (\<lambda>x. f)"
 
diff -r ff2a637a449e -r fc5066122e68 src/HOL/Auth/Message.thy
--- a/src/HOL/Auth/Message.thy	Fri Oct 18 11:44:05 2024 +0200
+++ b/src/HOL/Auth/Message.thy	Fri Oct 18 14:20:09 2024 +0200
@@ -51,6 +51,8 @@
 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
+  "_MTuple" \<rightleftharpoons> 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 ff2a637a449e -r fc5066122e68 src/HOL/Codegenerator_Test/Code_Lazy_Test.thy
--- a/src/HOL/Codegenerator_Test/Code_Lazy_Test.thy	Fri Oct 18 11:44:05 2024 +0200
+++ b/src/HOL/Codegenerator_Test/Code_Lazy_Test.thy	Fri Oct 18 14:20:09 2024 +0200
@@ -25,6 +25,8 @@
 no_notation lazy_llist (\<open>_\<close>)
 syntax
   "_llist" :: "args => 'a list"  (\<open>(\<open>indent=1 notation=\<open>mixfix lazy list enumeration\<close>\<close>\<^bold>[_\<^bold>])\<close>)
+syntax_consts
+  "_llist" \<rightleftharpoons> lazy_llist
 translations
   "\<^bold>[x, xs\<^bold>]" == "x\<^bold>#\<^bold>[xs\<^bold>]"
   "\<^bold>[x\<^bold>]" == "x\<^bold>#\<^bold>[\<^bold>]"
diff -r ff2a637a449e -r fc5066122e68 src/HOL/Computational_Algebra/Polynomial.thy
--- a/src/HOL/Computational_Algebra/Polynomial.thy	Fri Oct 18 11:44:05 2024 +0200
+++ b/src/HOL/Computational_Algebra/Polynomial.thy	Fri Oct 18 14:20:09 2024 +0200
@@ -350,6 +350,8 @@
 
 syntax
   "_poly" :: "args \<Rightarrow> 'a poly"  (\<open>(\<open>indent=2 notation=\<open>mixfix polynomial enumeration\<close>\<close>[:_:])\<close>)
+syntax_consts
+  "_poly" \<rightleftharpoons> pCons
 translations
   "[:x, xs:]" \<rightleftharpoons> "CONST pCons x [:xs:]"
   "[:x:]" \<rightleftharpoons> "CONST pCons x 0"
diff -r ff2a637a449e -r fc5066122e68 src/HOL/Filter.thy
--- a/src/HOL/Filter.thy	Fri Oct 18 11:44:05 2024 +0200
+++ b/src/HOL/Filter.thy	Fri Oct 18 14:20:09 2024 +0200
@@ -1308,10 +1308,8 @@
 
 syntax
   "_LIM" :: "pttrns \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'a \<Rightarrow> bool" (\<open>(\<open>indent=3 notation=\<open>binder LIM\<close>\<close>LIM (_)/ (_)./ (_) :> (_))\<close> [1000, 10, 0, 10] 10)
-
 syntax_consts
   "_LIM" == filterlim
-
 translations
   "LIM x F1. f :> F2" == "CONST filterlim (\<lambda>x. f) F2 F1"
 
diff -r ff2a637a449e -r fc5066122e68 src/HOL/Fun.thy
--- a/src/HOL/Fun.thy	Fri Oct 18 11:44:05 2024 +0200
+++ b/src/HOL/Fun.thy	Fri Oct 18 14:20:09 2024 +0200
@@ -846,7 +846,8 @@
   "_updbinds":: "updbind \<Rightarrow> updbinds \<Rightarrow> updbinds" (\<open>_,/ _\<close>)
   "_Update"  :: "'a \<Rightarrow> updbinds \<Rightarrow> 'a"
     (\<open>(\<open>open_block notation=\<open>mixfix function update\<close>\<close>_/'((2_)'))\<close> [1000, 0] 900)
-
+syntax_consts
+  "_Update" \<rightleftharpoons> 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 ff2a637a449e -r fc5066122e68 src/HOL/HOLCF/Sprod.thy
--- a/src/HOL/HOLCF/Sprod.thy	Fri Oct 18 11:44:05 2024 +0200
+++ b/src/HOL/HOLCF/Sprod.thy	Fri Oct 18 14:20:09 2024 +0200
@@ -42,6 +42,8 @@
 
 syntax
   "_stuple" :: "[logic, args] \<Rightarrow> logic"  (\<open>(\<open>indent=1 notation=\<open>mixfix strict tuple\<close>\<close>'(:_,/ _:'))\<close>)
+syntax_consts
+  "_stuple" \<rightleftharpoons> spair
 translations
   "(:x, y, z:)" \<rightleftharpoons> "(:x, (:y, z:):)"
   "(:x, y:)" \<rightleftharpoons> "CONST spair\<cdot>x\<cdot>y"
diff -r ff2a637a449e -r fc5066122e68 src/HOL/HOLCF/ex/Letrec.thy
--- a/src/HOL/HOLCF/ex/Letrec.thy	Fri Oct 18 11:44:05 2024 +0200
+++ b/src/HOL/HOLCF/ex/Letrec.thy	Fri Oct 18 14:20:09 2024 +0200
@@ -22,6 +22,9 @@
   "_recbinds" :: "[recbindt, recbinds] \<Rightarrow> recbinds"  (\<open>_;/ _\<close>)
   "_Letrec"   :: "[recbinds, logic] \<Rightarrow> logic"        (\<open>(\<open>notation=\<open>mixfix Letrec expression\<close>\<close>Letrec (_)/ in (_))\<close> 10)
 
+syntax_consts
+  "_Letrec" \<rightleftharpoons> CLetrec
+
 translations
   (recbindt) "x = a, (y,ys) = (b,bs)" == (recbindt) "(x,y,ys) = (a,b,bs)"
   (recbindt) "x = a, y = b"          == (recbindt) "(x,y) = (a,b)"
diff -r ff2a637a449e -r fc5066122e68 src/HOL/Library/FSet.thy
--- a/src/HOL/Library/FSet.thy	Fri Oct 18 11:44:05 2024 +0200
+++ b/src/HOL/Library/FSet.thy	Fri Oct 18 14:20:09 2024 +0200
@@ -166,6 +166,8 @@
 
 syntax
   "_fset" :: "args => 'a fset"  (\<open>(\<open>indent=2 notation=\<open>mixfix finite set enumeration\<close>\<close>{|_|})\<close>)
+syntax_consts
+  "_fset" \<rightleftharpoons> finsert
 translations
   "{|x, xs|}" == "CONST finsert x {|xs|}"
   "{|x|}"     == "CONST finsert x {||}"
diff -r ff2a637a449e -r fc5066122e68 src/HOL/Library/Multiset.thy
--- a/src/HOL/Library/Multiset.thy	Fri Oct 18 11:44:05 2024 +0200
+++ b/src/HOL/Library/Multiset.thy	Fri Oct 18 14:20:09 2024 +0200
@@ -93,6 +93,8 @@
 
 syntax
   "_multiset" :: "args \<Rightarrow> 'a multiset"  (\<open>(\<open>indent=2 notation=\<open>mixfix multiset enumeration\<close>\<close>{#_#})\<close>)
+syntax_consts
+  "_multiset" \<rightleftharpoons> add_mset
 translations
   "{#x, xs#}" == "CONST add_mset x {#xs#}"
   "{#x#}" == "CONST add_mset x {#}"
diff -r ff2a637a449e -r fc5066122e68 src/HOL/List.thy
--- a/src/HOL/List.thy	Fri Oct 18 11:44:05 2024 +0200
+++ b/src/HOL/List.thy	Fri Oct 18 14:20:09 2024 +0200
@@ -56,6 +56,8 @@
 syntax
   "_list" :: "args \<Rightarrow> 'a list"  (\<open>(\<open>indent=1 notation=\<open>mixfix list enumeration\<close>\<close>[_])\<close>)
 end
+syntax_consts
+  "_list" \<rightleftharpoons> Cons
 translations
   "[x, xs]" \<rightleftharpoons> "x#[xs]"
   "[x]" \<rightleftharpoons> "x#[]"
@@ -144,7 +146,8 @@
   "_lupdbinds" :: "[lupdbind, lupdbinds] => lupdbinds"    (\<open>_,/ _\<close>)
   "_LUpdate" :: "['a, lupdbinds] => 'a"
     (\<open>(\<open>open_block notation=\<open>mixfix list update\<close>\<close>_/[(_)])\<close> [1000,0] 900)
-
+syntax_consts
+  "_LUpdate" \<rightleftharpoons> list_update
 translations
   "_LUpdate xs (_lupdbinds b bs)" == "_LUpdate (_LUpdate xs b) bs"
   "xs[i:=x]" == "CONST list_update xs i x"
diff -r ff2a637a449e -r fc5066122e68 src/HOL/Metis_Examples/Message.thy
--- a/src/HOL/Metis_Examples/Message.thy	Fri Oct 18 11:44:05 2024 +0200
+++ b/src/HOL/Metis_Examples/Message.thy	Fri Oct 18 14:20:09 2024 +0200
@@ -50,6 +50,8 @@
 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
+  "_MTuple" \<rightleftharpoons> 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 ff2a637a449e -r fc5066122e68 src/HOL/Probability/Probability_Measure.thy
--- a/src/HOL/Probability/Probability_Measure.thy	Fri Oct 18 11:44:05 2024 +0200
+++ b/src/HOL/Probability/Probability_Measure.thy	Fri Oct 18 14:20:09 2024 +0200
@@ -249,10 +249,8 @@
 
 syntax
   "_prob" :: "pttrn \<Rightarrow> logic \<Rightarrow> logic \<Rightarrow> logic" (\<open>('\<P>'((/_ in _./ _)'))\<close>)
-
 syntax_consts
   "_prob" == measure
-
 translations
   "\<P>(x in M. P)" => "CONST measure M {x \<in> CONST space M. P}"
 
@@ -324,10 +322,8 @@
 
 syntax
   "_conditional_prob" :: "pttrn \<Rightarrow> logic \<Rightarrow> logic \<Rightarrow> logic \<Rightarrow> logic" (\<open>('\<P>'(_ in _. _ \<bar>/ _'))\<close>)
-
 syntax_consts
   "_conditional_prob" == cond_prob
-
 translations
   "\<P>(x in M. P \<bar> Q)" => "CONST cond_prob M (\<lambda>x. P) (\<lambda>x. Q)"
 
diff -r ff2a637a449e -r fc5066122e68 src/HOL/Prolog/Test.thy
--- a/src/HOL/Prolog/Test.thy	Fri Oct 18 11:44:05 2024 +0200
+++ b/src/HOL/Prolog/Test.thy	Fri Oct 18 14:20:09 2024 +0200
@@ -20,6 +20,8 @@
 
 syntax
   "_list" :: "args => 'a list"  (\<open>(\<open>indent=1 notation=\<open>mixfix list enumeration\<close>\<close>[_])\<close>)
+syntax_consts
+  "_list" \<rightleftharpoons> Cons
 translations
   "[x, xs]" == "x#[xs]"
   "[x]" == "x#[]"
diff -r ff2a637a449e -r fc5066122e68 src/HOL/Quotient_Examples/Lift_FSet.thy
--- a/src/HOL/Quotient_Examples/Lift_FSet.thy	Fri Oct 18 11:44:05 2024 +0200
+++ b/src/HOL/Quotient_Examples/Lift_FSet.thy	Fri Oct 18 14:20:09 2024 +0200
@@ -97,6 +97,8 @@
 
 syntax
   "_fset" :: "args => 'a fset"  (\<open>(\<open>indent=2 notation=\<open>mixfix finite set enumeration\<close>\<close>{|_|})\<close>)
+syntax_consts
+  "_fset" == fcons
 translations
   "{|x, xs|}" == "CONST fcons x {|xs|}"
   "{|x|}"     == "CONST fcons x {||}"
diff -r ff2a637a449e -r fc5066122e68 src/HOL/Quotient_Examples/Quotient_FSet.thy
--- a/src/HOL/Quotient_Examples/Quotient_FSet.thy	Fri Oct 18 11:44:05 2024 +0200
+++ b/src/HOL/Quotient_Examples/Quotient_FSet.thy	Fri Oct 18 14:20:09 2024 +0200
@@ -290,6 +290,8 @@
 
 syntax
   "_fset" :: "args => 'a fset"  (\<open>(\<open>indent=2 notation=\<open>mixfix finite set enumeration\<close>\<close>{|_|})\<close>)
+syntax_consts
+  "_fset" \<rightleftharpoons> insert_fset
 translations
   "{|x, xs|}" == "CONST insert_fset x {|xs|}"
   "{|x|}"     == "CONST insert_fset x {||}"
diff -r ff2a637a449e -r fc5066122e68 src/HOL/SET_Protocol/Message_SET.thy
--- a/src/HOL/SET_Protocol/Message_SET.thy	Fri Oct 18 11:44:05 2024 +0200
+++ b/src/HOL/SET_Protocol/Message_SET.thy	Fri Oct 18 14:20:09 2024 +0200
@@ -70,6 +70,8 @@
 (*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
+  "_MTuple" \<rightleftharpoons> 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 ff2a637a449e -r fc5066122e68 src/HOL/SPARK/SPARK_Setup.thy
--- a/src/HOL/SPARK/SPARK_Setup.thy	Fri Oct 18 11:44:05 2024 +0200
+++ b/src/HOL/SPARK/SPARK_Setup.thy	Fri Oct 18 14:20:09 2024 +0200
@@ -55,11 +55,9 @@
   "fun_upds f xs y z = (if z \<in> xs then y else f z)"
 
 syntax
-  "_updsbind" :: "['a, 'a] => updbind"             (\<open>(2_ [:=]/ _)\<close>)
-
+  "_updsbind" :: "['a, 'a] => updbind"  (\<open>(\<open>indent=2 notation=\<open>infix update set\<close>\<close>_ [:=]/ _)\<close>)
 syntax_consts
   "_updsbind" == fun_upds
-
 translations
   "f(xs[:=]y)" == "CONST fun_upds f xs y"
 
diff -r ff2a637a449e -r fc5066122e68 src/HOL/Set.thy
--- a/src/HOL/Set.thy	Fri Oct 18 11:44:05 2024 +0200
+++ b/src/HOL/Set.thy	Fri Oct 18 14:20:09 2024 +0200
@@ -43,6 +43,8 @@
 
 syntax
   "_Coll" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a set"    (\<open>(\<open>indent=1 notation=\<open>mixfix set comprehension\<close>\<close>{_./ _})\<close>)
+syntax_consts
+  "_Coll" \<rightleftharpoons> Collect
 translations
   "{x. P}" \<rightleftharpoons> "CONST Collect (\<lambda>x. P)"
 
@@ -156,6 +158,8 @@
 
 syntax
   "_Finset" :: "args \<Rightarrow> 'a set"  (\<open>(\<open>indent=1 notation=\<open>mixfix set enumeration\<close>\<close>{_})\<close>)
+syntax_consts
+  "_Finset" \<rightleftharpoons> insert
 translations
   "{x, xs}" \<rightleftharpoons> "CONST insert x {xs}"
   "{x}" \<rightleftharpoons> "CONST insert x {}"
diff -r ff2a637a449e -r fc5066122e68 src/HOL/UNITY/Union.thy
--- a/src/HOL/UNITY/Union.thy	Fri Oct 18 11:44:05 2024 +0200
+++ b/src/HOL/UNITY/Union.thy	Fri Oct 18 14:20:09 2024 +0200
@@ -39,8 +39,8 @@
   where "safety_prop X \<longleftrightarrow> SKIP \<in> X \<and> (\<forall>G. Acts G \<subseteq> \<Union>(Acts ` X) \<longrightarrow> G \<in> X)"
 
 syntax
-  "_JOIN1" :: "[pttrns, 'b set] => 'b set"              (\<open>(3\<Squnion>_./ _)\<close> 10)
-  "_JOIN"  :: "[pttrn, 'a set, 'b set] => 'b set"       (\<open>(3\<Squnion>_\<in>_./ _)\<close> 10)
+  "_JOIN1" :: "[pttrns, 'b set] => 'b set"  (\<open>(\<open>indent=3 notation=\<open>binder \<Squnion>\<close>\<close>\<Squnion>_./ _)\<close> 10)
+  "_JOIN"  :: "[pttrn, 'a set, 'b set] => 'b set"  (\<open>(\<open>indent=3 notation=\<open>binder \<Squnion>\<close>\<close>\<Squnion>_\<in>_./ _)\<close> 10)
 syntax_consts
   "_JOIN1" "_JOIN" == JOIN
 translations
diff -r ff2a637a449e -r fc5066122e68 src/HOL/ex/Code_Lazy_Demo.thy
--- a/src/HOL/ex/Code_Lazy_Demo.thy	Fri Oct 18 11:44:05 2024 +0200
+++ b/src/HOL/ex/Code_Lazy_Demo.thy	Fri Oct 18 14:20:09 2024 +0200
@@ -41,6 +41,8 @@
 
 syntax
   "_llist" :: "args => 'a list"  (\<open>(\<open>indent=1 notation=\<open>mixfix lazy list enumeration\<close>\<close>\<^bold>\<lbrakk>_\<^bold>\<rbrakk>)\<close>)
+syntax_consts
+  "_llist" == LCons
 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 ff2a637a449e -r fc5066122e68 src/Pure/Examples/Higher_Order_Logic.thy
--- a/src/Pure/Examples/Higher_Order_Logic.thy	Fri Oct 18 11:44:05 2024 +0200
+++ b/src/Pure/Examples/Higher_Order_Logic.thy	Fri Oct 18 14:20:09 2024 +0200
@@ -401,7 +401,7 @@
 axiomatization Eps :: "('a \<Rightarrow> o) \<Rightarrow> 'a"
   where someI: "P x \<Longrightarrow> P (Eps P)"
 
-syntax "_Eps" :: "pttrn \<Rightarrow> o \<Rightarrow> 'a"  (\<open>(3SOME _./ _)\<close> [0, 10] 10)
+syntax "_Eps" :: "pttrn \<Rightarrow> o \<Rightarrow> 'a"  (\<open>(\<open>indent=3 notation=\<open>binder SOME\<close>\<close>SOME _./ _)\<close> [0, 10] 10)
 syntax_consts "_Eps" \<rightleftharpoons> Eps
 translations "SOME x. P" \<rightleftharpoons> "CONST Eps (\<lambda>x. P)"
 
diff -r ff2a637a449e -r fc5066122e68 src/Pure/pure_thy.ML
--- a/src/Pure/pure_thy.ML	Fri Oct 18 11:44:05 2024 +0200
+++ b/src/Pure/pure_thy.ML	Fri Oct 18 14:20:09 2024 +0200
@@ -172,7 +172,8 @@
     ("_position",   typ "float_token \<Rightarrow> float_position", Mixfix.mixfix "_"),
     ("_constify",   typ "num_position \<Rightarrow> num_const",   Mixfix.mixfix "_"),
     ("_constify",   typ "float_position \<Rightarrow> float_const", Mixfix.mixfix "_"),
-    ("_index",      typ "logic \<Rightarrow> index",              Mixfix.mixfix "(\<open>unbreakable\<close>\<^bsub>_\<^esub>)"),
+    ("_index",      typ "logic \<Rightarrow> index",
+      Mixfix.mixfix "(\<open>unbreakable notation=\<open>mixfix index\<close>\<close>\<^bsub>_\<^esub>)"),
     ("_indexdefault", typ "index",                     Mixfix.mixfix ""),
     ("_indexvar",   typ "index",                       Mixfix.mixfix "'\<index>"),
     ("_struct",     typ "index \<Rightarrow> logic",              NoSyn),
@@ -251,7 +252,10 @@
   #> Sign.parse_translation Syntax_Trans.pure_parse_translation
   #> Sign.print_ast_translation Syntax_Trans.pure_print_ast_translation
   #> Sign.syntax_deps
-   [("_bracket", ["\<^type>fun"]), ("_bigimpl", ["\<^const>Pure.imp"])]
+   [("_bracket", ["\<^type>fun"]),
+    ("_bigimpl", ["\<^const>Pure.imp"]),
+    ("_TYPE", ["\<^const>Pure.type"]),
+    ("_TERM", ["\<^const>Pure.term"])]
   #> Sign.add_consts
    [(qualify (Binding.make ("term", \<^here>)), typ "'a \<Rightarrow> prop", NoSyn),
     (qualify (Binding.make ("sort_constraint", \<^here>)), typ "'a itself \<Rightarrow> prop", NoSyn),
diff -r ff2a637a449e -r fc5066122e68 src/ZF/Induct/Multiset.thy
--- a/src/ZF/Induct/Multiset.thy	Fri Oct 18 11:44:05 2024 +0200
+++ b/src/ZF/Induct/Multiset.thy	Fri Oct 18 14:20:09 2024 +0200
@@ -75,6 +75,8 @@
 
 syntax
   "_MColl" :: "[pttrn, i, o] \<Rightarrow> i" (\<open>(\<open>indent=1 notation=\<open>mixfix multiset comprehension\<close>\<close>{# _ \<in> _./ _#})\<close>)
+syntax_consts
+  "_MColl" \<rightleftharpoons> MCollect
 translations
   "{#x \<in> M. P#}" == "CONST MCollect(M, \<lambda>x. P)"
 
diff -r ff2a637a449e -r fc5066122e68 src/ZF/ZF_Base.thy
--- a/src/ZF/ZF_Base.thy	Fri Oct 18 11:44:05 2024 +0200
+++ b/src/ZF/ZF_Base.thy	Fri Oct 18 14:20:09 2024 +0200
@@ -56,6 +56,8 @@
 
 syntax
   "_Replace" :: "[pttrn, pttrn, i, o] \<Rightarrow> i"  (\<open>(\<open>indent=1 notation=\<open>mixfix relational replacement\<close>\<close>{_ ./ _ \<in> _, _})\<close>)
+syntax_consts
+  "_Replace" \<rightleftharpoons> Replace
 translations
   "{y. x\<in>A, Q}" \<rightleftharpoons> "CONST Replace(A, \<lambda>x y. Q)"
 
@@ -67,6 +69,8 @@
 
 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" \<rightleftharpoons> RepFun
 translations
   "{b. x\<in>A}" \<rightleftharpoons> "CONST RepFun(A, \<lambda>x. b)"
 
@@ -77,6 +81,8 @@
 
 syntax
   "_Collect" :: "[pttrn, i, o] \<Rightarrow> i"  (\<open>(\<open>indent=1 notation=\<open>mixfix set comprehension\<close>\<close>{_ \<in> _ ./ _})\<close>)
+syntax_consts
+  "_Collect" \<rightleftharpoons> Collect
 translations
   "{x\<in>A. P}" \<rightleftharpoons> "CONST Collect(A, \<lambda>x. P)"
 
diff -r ff2a637a449e -r fc5066122e68 src/ZF/func.thy
--- a/src/ZF/func.thy	Fri Oct 18 11:44:05 2024 +0200
+++ b/src/ZF/func.thy	Fri Oct 18 14:20:09 2024 +0200
@@ -452,6 +452,8 @@
   ""            :: "updbind \<Rightarrow> updbinds"  (\<open>_\<close>)
   "_updbinds"   :: "[updbind, updbinds] \<Rightarrow> updbinds"  (\<open>_,/ _\<close>)
   "_Update"     :: "[i, updbinds] \<Rightarrow> i"  (\<open>(\<open>open_block notation=\<open>mixfix function update\<close>\<close>_/'((_)'))\<close> [900,0] 900)
+syntax_consts
+  "_Update" \<rightleftharpoons> update
 translations
   "_Update (f, _updbinds(b,bs))"  == "_Update (_Update(f,b), bs)"
   "f(x:=y)"                       == "CONST update(f,x,y)"