# HG changeset patch
# User wenzelm
# Date 1724590939 -7200
# Node ID be8c0e039a5ed82d88998bb2d77ae3d78ce99582
# Parent  4641f0fdaa59585aadd63778a180eed4a31da0c1
more markup for syntax consts;

diff -r 4641f0fdaa59 -r be8c0e039a5e src/HOL/BNF_Cardinal_Arithmetic.thy
--- a/src/HOL/BNF_Cardinal_Arithmetic.thy	Sun Aug 25 12:43:43 2024 +0200
+++ b/src/HOL/BNF_Cardinal_Arithmetic.thy	Sun Aug 25 15:02:19 2024 +0200
@@ -275,6 +275,9 @@
   "pttrn => ('a * 'a) set => 'b * 'b set => (('a * 'b) * ('a * 'b)) set"
   ("(3CSUM _:_. _)" [0, 51, 10] 10)
 
+syntax_consts
+  "_Csum" == Csum
+
 translations
   "CSUM i:r. rs" == "CONST Csum r (%i. rs)"
 
diff -r 4641f0fdaa59 -r be8c0e039a5e src/HOL/Complete_Lattices.thy
--- a/src/HOL/Complete_Lattices.thy	Sun Aug 25 12:43:43 2024 +0200
+++ b/src/HOL/Complete_Lattices.thy	Sun Aug 25 15:02:19 2024 +0200
@@ -32,6 +32,10 @@
   "_SUP1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           ("(3\<Squnion>_./ _)" [0, 10] 10)
   "_SUP"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b"  ("(3\<Squnion>_\<in>_./ _)" [0, 0, 10] 10)
 
+syntax_consts
+  "_INF1" "_INF" \<rightleftharpoons> Inf and
+  "_SUP1" "_SUP" \<rightleftharpoons> Sup
+
 translations
   "\<Sqinter>x y. f"   \<rightleftharpoons> "\<Sqinter>x. \<Sqinter>y. f"
   "\<Sqinter>x. f"     \<rightleftharpoons> "\<Sqinter>(CONST range (\<lambda>x. f))"
@@ -850,6 +854,9 @@
   "_INTER1"     :: "pttrns \<Rightarrow> 'b set \<Rightarrow> 'b set"           ("(3\<Inter>(\<open>unbreakable\<close>\<^bsub>_\<^esub>)/ _)" [0, 10] 10)
   "_INTER"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b set \<Rightarrow> 'b set"  ("(3\<Inter>(\<open>unbreakable\<close>\<^bsub>_\<in>_\<^esub>)/ _)" [0, 0, 10] 10)
 
+syntax_consts
+  "_INTER1" "_INTER" \<rightleftharpoons> Inter
+
 translations
   "\<Inter>x y. f"  \<rightleftharpoons> "\<Inter>x. \<Inter>y. f"
   "\<Inter>x. f"    \<rightleftharpoons> "\<Inter>(CONST range (\<lambda>x. f))"
@@ -1013,6 +1020,9 @@
   "_UNION1"     :: "pttrns => 'b set => 'b set"           ("(3\<Union>(\<open>unbreakable\<close>\<^bsub>_\<^esub>)/ _)" [0, 10] 10)
   "_UNION"      :: "pttrn => 'a set => 'b set => 'b set"  ("(3\<Union>(\<open>unbreakable\<close>\<^bsub>_\<in>_\<^esub>)/ _)" [0, 0, 10] 10)
 
+syntax_consts
+  "_UNION1" "_UNION" \<rightleftharpoons> Union
+
 translations
   "\<Union>x y. f"   \<rightleftharpoons> "\<Union>x. \<Union>y. f"
   "\<Union>x. f"     \<rightleftharpoons> "\<Union>(CONST range (\<lambda>x. f))"
diff -r 4641f0fdaa59 -r be8c0e039a5e src/HOL/Filter.thy
--- a/src/HOL/Filter.thy	Sun Aug 25 12:43:43 2024 +0200
+++ b/src/HOL/Filter.thy	Sun Aug 25 15:02:19 2024 +0200
@@ -41,6 +41,8 @@
 
 syntax
   "_eventually" :: "pttrn => 'a filter => bool => bool"  ("(3\<forall>\<^sub>F _ in _./ _)" [0, 0, 10] 10)
+syntax_consts
+  "_eventually" == eventually
 translations
   "\<forall>\<^sub>Fx in F. P" == "CONST eventually (\<lambda>x. P) F"
 
@@ -159,6 +161,8 @@
 
 syntax
   "_frequently" :: "pttrn \<Rightarrow> 'a filter \<Rightarrow> bool \<Rightarrow> bool"  ("(3\<exists>\<^sub>F _ in _./ _)" [0, 0, 10] 10)
+syntax_consts
+  "_frequently" == frequently
 translations
   "\<exists>\<^sub>Fx in F. P" == "CONST frequently (\<lambda>x. P) F"
 
@@ -1305,6 +1309,9 @@
 syntax
   "_LIM" :: "pttrns \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'a \<Rightarrow> bool" ("(3LIM (_)/ (_)./ (_) :> (_))" [1000, 10, 0, 10] 10)
 
+syntax_consts
+  "_LIM" == filterlim
+
 translations
   "LIM x F1. f :> F2" == "CONST filterlim (\<lambda>x. f) F2 F1"
 
diff -r 4641f0fdaa59 -r be8c0e039a5e src/HOL/Fun.thy
--- a/src/HOL/Fun.thy	Sun Aug 25 12:43:43 2024 +0200
+++ b/src/HOL/Fun.thy	Sun Aug 25 15:02:19 2024 +0200
@@ -846,6 +846,9 @@
   "_updbinds":: "updbind \<Rightarrow> updbinds \<Rightarrow> updbinds" ("_,/ _")
   "_Update"  :: "'a \<Rightarrow> updbinds \<Rightarrow> 'a"            ("_/'((_)')" [1000, 0] 900)
 
+syntax_consts
+  "_updbind" "_updbinds" "_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 4641f0fdaa59 -r be8c0e039a5e src/HOL/GCD.thy
--- a/src/HOL/GCD.thy	Sun Aug 25 12:43:43 2024 +0200
+++ b/src/HOL/GCD.thy	Sun Aug 25 15:02:19 2024 +0200
@@ -153,6 +153,10 @@
   "_LCM1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           ("(3LCM _./ _)" [0, 10] 10)
   "_LCM"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b"  ("(3LCM _\<in>_./ _)" [0, 0, 10] 10)
 
+syntax_consts
+  "_GCD1" "_GCD" \<rightleftharpoons> Gcd and
+  "_LCM1" "_LCM" \<rightleftharpoons> Lcm
+
 translations
   "GCD x y. f"   \<rightleftharpoons> "GCD x. GCD y. f"
   "GCD x. f"     \<rightleftharpoons> "CONST Gcd (CONST range (\<lambda>x. f))"
@@ -2933,6 +2937,8 @@
 
 syntax "_type_char" :: "type => nat" ("(1CHAR/(1'(_')))")
 
+syntax_consts "_type_char" == semiring_char
+
 translations "CHAR('t)" => "CONST semiring_char (CONST Pure.type :: 't itself)"
 
 print_translation \<open>
diff -r 4641f0fdaa59 -r be8c0e039a5e src/HOL/Groups_Big.thy
--- a/src/HOL/Groups_Big.thy	Sun Aug 25 12:43:43 2024 +0200
+++ b/src/HOL/Groups_Big.thy	Sun Aug 25 15:02:19 2024 +0200
@@ -654,6 +654,8 @@
   "_sum" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b::comm_monoid_add"  ("(3SUM (_/:_)./ _)" [0, 51, 10] 10)
 syntax
   "_sum" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b::comm_monoid_add"  ("(2\<Sum>(_/\<in>_)./ _)" [0, 51, 10] 10)
+syntax_consts
+  "_sum" \<rightleftharpoons> sum
 translations \<comment> \<open>Beware of argument permutation!\<close>
   "\<Sum>i\<in>A. b" \<rightleftharpoons> "CONST sum (\<lambda>i. b) A"
 
@@ -663,6 +665,9 @@
   "_qsum" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a"  ("(3SUM _ |/ _./ _)" [0, 0, 10] 10)
 syntax
   "_qsum" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a"  ("(2\<Sum>_ | (_)./ _)" [0, 0, 10] 10)
+syntax_consts
+  "_qsum" == sum
+
 translations
   "\<Sum>x|P. t" => "CONST sum (\<lambda>x. t) {x. P}"
 
@@ -1415,6 +1420,8 @@
   "_prod" :: "pttrn => 'a set => 'b => 'b::comm_monoid_mult"  ("(4PROD (_/:_)./ _)" [0, 51, 10] 10)
 syntax
   "_prod" :: "pttrn => 'a set => 'b => 'b::comm_monoid_mult"  ("(2\<Prod>(_/\<in>_)./ _)" [0, 51, 10] 10)
+syntax_consts
+  "_prod" == prod
 translations \<comment> \<open>Beware of argument permutation!\<close>
   "\<Prod>i\<in>A. b" == "CONST prod (\<lambda>i. b) A"
 
@@ -1424,6 +1431,8 @@
   "_qprod" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a"  ("(4PROD _ |/ _./ _)" [0, 0, 10] 10)
 syntax
   "_qprod" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a"  ("(2\<Prod>_ | (_)./ _)" [0, 0, 10] 10)
+syntax_consts
+  "_qprod" == prod
 translations
   "\<Prod>x|P. t" => "CONST prod (\<lambda>x. t) {x. P}"
 
diff -r 4641f0fdaa59 -r be8c0e039a5e src/HOL/Groups_List.thy
--- a/src/HOL/Groups_List.thy	Sun Aug 25 12:43:43 2024 +0200
+++ b/src/HOL/Groups_List.thy	Sun Aug 25 15:02:19 2024 +0200
@@ -101,6 +101,8 @@
   "_sum_list" :: "pttrn => 'a list => 'b => 'b"    ("(3SUM _<-_. _)" [0, 51, 10] 10)
 syntax
   "_sum_list" :: "pttrn => 'a list => 'b => 'b"    ("(3\<Sum>_\<leftarrow>_. _)" [0, 51, 10] 10)
+syntax_consts
+  "_sum_list" == sum_list
 translations \<comment> \<open>Beware of argument permutation!\<close>
   "\<Sum>x\<leftarrow>xs. b" == "CONST sum_list (CONST map (\<lambda>x. b) xs)"
 
@@ -598,6 +600,8 @@
   "_prod_list" :: "pttrn => 'a list => 'b => 'b"    ("(3PROD _<-_. _)" [0, 51, 10] 10)
 syntax
   "_prod_list" :: "pttrn => 'a list => 'b => 'b"    ("(3\<Prod>_\<leftarrow>_. _)" [0, 51, 10] 10)
+syntax_consts
+  "_prod_list" \<rightleftharpoons> prod_list
 translations \<comment> \<open>Beware of argument permutation!\<close>
   "\<Prod>x\<leftarrow>xs. b" \<rightleftharpoons> "CONST prod_list (CONST map (\<lambda>x. b) xs)"
 
diff -r 4641f0fdaa59 -r be8c0e039a5e src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Sun Aug 25 12:43:43 2024 +0200
+++ b/src/HOL/HOL.thy	Sun Aug 25 15:02:19 2024 +0200
@@ -129,6 +129,9 @@
 
 syntax (ASCII) "_Uniq" :: "pttrn \<Rightarrow> bool \<Rightarrow> bool"  ("(4?< _./ _)" [0, 10] 10)
 syntax "_Uniq" :: "pttrn \<Rightarrow> bool \<Rightarrow> bool"  ("(2\<exists>\<^sub>\<le>\<^sub>1 _./ _)" [0, 10] 10)
+
+syntax_consts "_Uniq" \<rightleftharpoons> Uniq
+
 translations "\<exists>\<^sub>\<le>\<^sub>1x. P" \<rightleftharpoons> "CONST Uniq (\<lambda>x. P)"
 
 print_translation \<open>
@@ -141,6 +144,9 @@
 syntax (input)
   "_Ex1" :: "pttrn \<Rightarrow> bool \<Rightarrow> bool"  ("(3?! _./ _)" [0, 10] 10)
 syntax "_Ex1" :: "pttrn \<Rightarrow> bool \<Rightarrow> bool"  ("(3\<exists>!_./ _)" [0, 10] 10)
+
+syntax_consts "_Ex1" \<rightleftharpoons> Ex1
+
 translations "\<exists>!x. P" \<rightleftharpoons> "CONST Ex1 (\<lambda>x. P)"
 
 print_translation \<open>
@@ -151,6 +157,9 @@
 syntax
   "_Not_Ex" :: "idts \<Rightarrow> bool \<Rightarrow> bool"  ("(3\<nexists>_./ _)" [0, 10] 10)
   "_Not_Ex1" :: "pttrn \<Rightarrow> bool \<Rightarrow> bool"  ("(3\<nexists>!_./ _)" [0, 10] 10)
+syntax_consts
+  "_Not_Ex" \<rightleftharpoons> Ex and
+  "_Not_Ex1" \<rightleftharpoons> Ex1
 translations
   "\<nexists>x. P" \<rightleftharpoons> "\<not> (\<exists>x. P)"
   "\<nexists>!x. P" \<rightleftharpoons> "\<not> (\<exists>!x. P)"
@@ -171,6 +180,7 @@
   where "A \<longleftrightarrow> B \<equiv> A = B"
 
 syntax "_The" :: "[pttrn, bool] \<Rightarrow> 'a"  ("(3THE _./ _)" [0, 10] 10)
+syntax_consts "_The" \<rightleftharpoons> The
 translations "THE x. P" \<rightleftharpoons> "CONST The (\<lambda>x. P)"
 print_translation \<open>
   [(\<^const_syntax>\<open>The\<close>, fn _ => fn [Abs abs] =>
@@ -227,6 +237,8 @@
 definition Let :: "'a \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'b"
   where "Let s f \<equiv> f s"
 
+syntax_consts
+  "_bind" "_binds" "_Let" \<rightleftharpoons> Let
 translations
   "_Let (_binds b bs) e"  \<rightleftharpoons> "_Let b (_Let bs e)"
   "let x = a in e"        \<rightleftharpoons> "CONST Let a (\<lambda>x. e)"
diff -r 4641f0fdaa59 -r be8c0e039a5e src/HOL/Hilbert_Choice.thy
--- a/src/HOL/Hilbert_Choice.thy	Sun Aug 25 12:43:43 2024 +0200
+++ b/src/HOL/Hilbert_Choice.thy	Sun Aug 25 15:02:19 2024 +0200
@@ -22,6 +22,9 @@
   "_Eps" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a"  ("(3@ _./ _)" [0, 10] 10)
 syntax
   "_Eps" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a"  ("(3SOME _./ _)" [0, 10] 10)
+
+syntax_consts "_Eps" \<rightleftharpoons> Eps
+
 translations
   "SOME x. P" \<rightleftharpoons> "CONST Eps (\<lambda>x. P)"
 
diff -r 4641f0fdaa59 -r be8c0e039a5e src/HOL/Lattices_Big.thy
--- a/src/HOL/Lattices_Big.thy	Sun Aug 25 12:43:43 2024 +0200
+++ b/src/HOL/Lattices_Big.thy	Sun Aug 25 15:02:19 2024 +0200
@@ -470,6 +470,10 @@
   "_MAX1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           ("(3MAX _./ _)" [0, 10] 10)
   "_MAX"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b"  ("(3MAX _\<in>_./ _)" [0, 0, 10] 10)
 
+syntax_consts
+  "_MIN1" "_MIN" \<rightleftharpoons> Min and
+  "_MAX1" "_MAX" \<rightleftharpoons> Max
+
 translations
   "MIN x y. f"   \<rightleftharpoons> "MIN x. MIN y. f"
   "MIN x. f"     \<rightleftharpoons> "CONST Min (CONST range (\<lambda>x. f))"
@@ -478,6 +482,7 @@
   "MAX x. f"     \<rightleftharpoons> "CONST Max (CONST range (\<lambda>x. f))"
   "MAX x\<in>A. f"   \<rightleftharpoons> "CONST Max ((\<lambda>x. f) ` A)"
 
+
 text \<open>An aside: \<^const>\<open>Min\<close>/\<^const>\<open>Max\<close> on linear orders as special case of \<^const>\<open>Inf_fin\<close>/\<^const>\<open>Sup_fin\<close>\<close>
 
 lemma Inf_fin_Min:
@@ -919,6 +924,8 @@
 syntax
   "_arg_min" :: "('b \<Rightarrow> 'a) \<Rightarrow> pttrn \<Rightarrow> bool \<Rightarrow> 'b"
     ("(3ARG'_MIN _ _./ _)" [1000, 0, 10] 10)
+syntax_consts
+  "_arg_min" \<rightleftharpoons> arg_min
 translations
   "ARG_MIN f x. P" \<rightleftharpoons> "CONST arg_min f (\<lambda>x. P)"
 
@@ -1036,6 +1043,8 @@
 syntax
   "_arg_max" :: "('b \<Rightarrow> 'a) \<Rightarrow> pttrn \<Rightarrow> bool \<Rightarrow> 'a"
     ("(3ARG'_MAX _ _./ _)" [1000, 0, 10] 10)
+syntax_consts
+  "_arg_max" \<rightleftharpoons> arg_max
 translations
   "ARG_MAX f x. P" \<rightleftharpoons> "CONST arg_max f (\<lambda>x. P)"
 
diff -r 4641f0fdaa59 -r be8c0e039a5e src/HOL/List.thy
--- a/src/HOL/List.thy	Sun Aug 25 12:43:43 2024 +0200
+++ b/src/HOL/List.thy	Sun Aug 25 15:02:19 2024 +0200
@@ -46,6 +46,9 @@
   \<comment> \<open>list Enumeration\<close>
   "_list" :: "args => 'a list"    ("[(_)]")
 
+syntax_consts
+  "_list" == Cons
+
 translations
   "[x, xs]" == "x#[xs]"
   "[x]" == "x#[]"
@@ -83,6 +86,8 @@
   "_filter" :: "[pttrn, 'a list, bool] => 'a list"  ("(1[_<-_./ _])")
 syntax
   "_filter" :: "[pttrn, 'a list, bool] => 'a list"  ("(1[_\<leftarrow>_ ./ _])")
+syntax_consts
+  "_filter" \<rightleftharpoons> filter
 translations
   "[x<-xs . P]" \<rightharpoonup> "CONST filter (\<lambda>x. P) xs"
 
@@ -132,6 +137,9 @@
   "_lupdbinds" :: "[lupdbind, lupdbinds] => lupdbinds"    ("_,/ _")
   "_LUpdate" :: "['a, lupdbinds] => 'a"    ("_/[(_)]" [1000,0] 900)
 
+syntax_consts
+  "_lupdbind" "_lupdbinds" "_LUpdate" == list_update
+
 translations
   "_LUpdate xs (_lupdbinds b bs)" == "_LUpdate (_LUpdate xs b) bs"
   "xs[i:=x]" == "CONST list_update xs i x"
diff -r 4641f0fdaa59 -r be8c0e039a5e src/HOL/Map.thy
--- a/src/HOL/Map.thy	Sun Aug 25 12:43:43 2024 +0200
+++ b/src/HOL/Map.thy	Sun Aug 25 15:02:19 2024 +0200
@@ -67,6 +67,9 @@
 syntax (ASCII)
   "_maplet"  :: "['a, 'a] \<Rightarrow> maplet"             ("_ /|->/ _")
 
+syntax_consts
+  "_maplet" "_Maplets" "_Map" \<rightleftharpoons> fun_upd
+
 translations
   "_Update f (_maplet x y)" \<rightleftharpoons> "f(x := CONST Some y)"
   "_Maplets m ms" \<rightharpoonup> "_updbinds m ms"
@@ -76,6 +79,7 @@
   "_Map (_maplet x y)"  \<leftharpoondown> "_Update (\<lambda>u. CONST None) (_maplet x y)"
   "_Map (_updbinds m (_maplet x y))"  \<leftharpoondown> "_Update (_Map m) (_maplet x y)"
 
+
 text \<open>Updating with lists:\<close>
 
 primrec map_of :: "('a \<times> 'b) list \<Rightarrow> 'a \<rightharpoonup> 'b" where
@@ -98,6 +102,9 @@
 syntax (ASCII)
   "_maplets" :: "['a, 'a] \<Rightarrow> maplet"             ("_ /[|->]/ _")
 
+syntax_consts
+  "_maplets" \<rightleftharpoons> map_upds
+
 translations
   "_Update m (_maplets xs ys)" \<rightleftharpoons> "CONST map_upds m xs ys"
 
diff -r 4641f0fdaa59 -r be8c0e039a5e src/HOL/Orderings.thy
--- a/src/HOL/Orderings.thy	Sun Aug 25 12:43:43 2024 +0200
+++ b/src/HOL/Orderings.thy	Sun Aug 25 15:02:19 2024 +0200
@@ -745,6 +745,10 @@
   "_All_neq" :: "[idt, 'a, bool] => bool"    ("(3! _~=_./ _)"  [0, 0, 10] 10)
   "_Ex_neq" :: "[idt, 'a, bool] => bool"    ("(3? _~=_./ _)"  [0, 0, 10] 10)
 
+syntax_consts
+  "_All_less" "_All_less_eq" "_All_greater" "_All_greater_eq" "_All_neq" \<rightleftharpoons> All and
+  "_Ex_less" "_Ex_less_eq" "_Ex_greater" "_Ex_greater_eq" "_Ex_neq" \<rightleftharpoons> Ex
+
 translations
   "\<forall>x<y. P" \<rightharpoonup> "\<forall>x. x < y \<longrightarrow> P"
   "\<exists>x<y. P" \<rightharpoonup> "\<exists>x. x < y \<and> P"
diff -r 4641f0fdaa59 -r be8c0e039a5e src/HOL/Product_Type.thy
--- a/src/HOL/Product_Type.thy	Sun Aug 25 12:43:43 2024 +0200
+++ b/src/HOL/Product_Type.thy	Sun Aug 25 15:02:19 2024 +0200
@@ -293,6 +293,10 @@
   ""            :: "pttrn \<Rightarrow> patterns"                  ("_")
   "_patterns"   :: "pttrn \<Rightarrow> patterns \<Rightarrow> patterns"      ("_,/ _")
   "_unit"       :: pttrn                                ("'(')")
+syntax_consts
+  "_tuple" "_tuple_arg" "_tuple_args" \<rightleftharpoons> Pair and
+  "_pattern" "_patterns" \<rightleftharpoons> case_prod and
+  "_unit" \<rightleftharpoons> case_unit
 translations
   "(x, y)" \<rightleftharpoons> "CONST Pair x y"
   "_pattern x y" \<rightleftharpoons> "CONST Pair x y"
@@ -1010,6 +1014,8 @@
 
 syntax
   "_Sigma" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b set \<Rightarrow> ('a \<times> 'b) set"  ("(3SIGMA _:_./ _)" [0, 0, 10] 10)
+syntax_consts
+  "_Sigma" \<rightleftharpoons> Sigma
 translations
   "SIGMA x:A. B" \<rightleftharpoons> "CONST Sigma A (\<lambda>x. B)"
 
diff -r 4641f0fdaa59 -r be8c0e039a5e src/HOL/Set.thy
--- a/src/HOL/Set.thy	Sun Aug 25 12:43:43 2024 +0200
+++ b/src/HOL/Set.thy	Sun Aug 25 15:02:19 2024 +0200
@@ -40,6 +40,8 @@
 
 syntax
   "_Coll" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a set"    ("(1{_./ _})")
+syntax_consts
+  "_Coll" \<rightleftharpoons> Collect
 translations
   "{x. P}" \<rightleftharpoons> "CONST Collect (\<lambda>x. P)"
 
@@ -47,6 +49,8 @@
   "_Collect" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> bool \<Rightarrow> 'a set"  ("(1{(_/: _)./ _})")
 syntax
   "_Collect" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> bool \<Rightarrow> 'a set"  ("(1{(_/ \<in> _)./ _})")
+syntax_consts
+  "_Collect" \<rightleftharpoons> Collect
 translations
   "{p:A. P}" \<rightharpoonup> "CONST Collect (\<lambda>p. p \<in> A \<and> P)"
 
@@ -141,6 +145,8 @@
 
 syntax
   "_Finset" :: "args \<Rightarrow> 'a set"    ("{(_)}")
+syntax_consts
+  "_Finset" \<rightleftharpoons> insert
 translations
   "{x, xs}" \<rightleftharpoons> "CONST insert x {xs}"
   "{x}" \<rightleftharpoons> "CONST insert x {}"
@@ -203,6 +209,12 @@
   "_Bex1"       :: "pttrn \<Rightarrow> 'a set \<Rightarrow> bool \<Rightarrow> bool"      ("(3\<exists>!(_/\<in>_)./ _)" [0, 0, 10] 10)
   "_Bleast"     :: "id \<Rightarrow> 'a set \<Rightarrow> bool \<Rightarrow> 'a"           ("(3LEAST(_/\<in>_)./ _)" [0, 0, 10] 10)
 
+syntax_consts
+  "_Ball" \<rightleftharpoons> Ball and
+  "_Bex" \<rightleftharpoons> Bex and
+  "_Bex1" \<rightleftharpoons> Ex1 and
+  "_Bleast" \<rightleftharpoons> Least
+
 translations
   "\<forall>x\<in>A. P" \<rightleftharpoons> "CONST Ball A (\<lambda>x. P)"
   "\<exists>x\<in>A. P" \<rightleftharpoons> "CONST Bex A (\<lambda>x. P)"
@@ -223,6 +235,11 @@
   "_setleEx"    :: "[idt, 'a, bool] \<Rightarrow> bool"   ("(3\<exists>_\<subseteq>_./ _)" [0, 0, 10] 10)
   "_setleEx1"   :: "[idt, 'a, bool] \<Rightarrow> bool"   ("(3\<exists>!_\<subseteq>_./ _)" [0, 0, 10] 10)
 
+syntax_consts
+  "_setlessAll" "_setleAll" \<rightleftharpoons> All and
+  "_setlessEx" "_setleEx" \<rightleftharpoons> Ex and
+  "_setleEx1" \<rightleftharpoons> Ex1
+
 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"
@@ -272,6 +289,8 @@
 
 syntax
   "_Setcompr" :: "'a \<Rightarrow> idts \<Rightarrow> bool \<Rightarrow> 'a set"    ("(1{_ |/_./ _})")
+syntax_consts
+  "_Setcompr" \<rightleftharpoons> Collect
 
 parse_translation \<open>
   let
diff -r 4641f0fdaa59 -r be8c0e039a5e src/HOL/Set_Interval.thy
--- a/src/HOL/Set_Interval.thy	Sun Aug 25 12:43:43 2024 +0200
+++ b/src/HOL/Set_Interval.thy	Sun Aug 25 15:02:19 2024 +0200
@@ -84,6 +84,10 @@
   "_INTER_le"   :: "'a => 'a => 'b set => 'b set"       ("(3\<Inter>_\<le>_./ _)" [0, 0, 10] 10)
   "_INTER_less" :: "'a => 'a => 'b set => 'b set"       ("(3\<Inter>_<_./ _)" [0, 0, 10] 10)
 
+syntax_consts
+  "_UNION_le" "_UNION_less" \<rightleftharpoons> Union and
+  "_INTER_le" "_INTER_less" \<rightleftharpoons> Inter
+
 translations
   "\<Union>i\<le>n. A" \<rightleftharpoons> "\<Union>i\<in>{..n}. A"
   "\<Union>i<n. A" \<rightleftharpoons> "\<Union>i\<in>{..<n}. A"
@@ -2005,6 +2009,9 @@
   "_upt_sum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b"  ("(3\<Sum>_<_./ _)" [0,0,10] 10)
   "_upto_sum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b"  ("(3\<Sum>_\<le>_./ _)" [0,0,10] 10)
 
+syntax_consts
+  "_from_to_sum" "_from_upto_sum" "_upt_sum" "_upto_sum" == sum
+
 translations
   "\<Sum>x=a..b. t" == "CONST sum (\<lambda>x. t) {a..b}"
   "\<Sum>x=a..<b. t" == "CONST sum (\<lambda>x. t) {a..<b}"
@@ -2695,6 +2702,9 @@
   "_upt_prod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b"  ("(3\<Prod>_<_./ _)" [0,0,10] 10)
   "_upto_prod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b"  ("(3\<Prod>_\<le>_./ _)" [0,0,10] 10)
 
+syntax_consts
+  "_from_to_prod" "_from_upto_prod" "_upt_prod" "_upto_prod" \<rightleftharpoons> prod
+
 translations
   "\<Prod>x=a..b. t" \<rightleftharpoons> "CONST prod (\<lambda>x. t) {a..b}"
   "\<Prod>x=a..<b. t" \<rightleftharpoons> "CONST prod (\<lambda>x. t) {a..<b}"
diff -r 4641f0fdaa59 -r be8c0e039a5e src/HOL/String.thy
--- a/src/HOL/String.thy	Sun Aug 25 12:43:43 2024 +0200
+++ b/src/HOL/String.thy	Sun Aug 25 15:02:19 2024 +0200
@@ -218,6 +218,8 @@
 syntax
   "_Char" :: "str_position \<Rightarrow> char"    ("CHR _")
   "_Char_ord" :: "num_const \<Rightarrow> char"   ("CHR _")
+syntax_consts
+  "_Char" "_Char_ord" \<rightleftharpoons> Char
 
 type_synonym string = "char list"
 
@@ -522,6 +524,8 @@
 syntax
   "_Literal" :: "str_position \<Rightarrow> String.literal"   ("STR _")
   "_Ascii" :: "num_const \<Rightarrow> String.literal"        ("STR _")
+syntax_consts
+  "_Literal" "_Ascii" \<rightleftharpoons> String.Literal
 
 ML_file \<open>Tools/literal.ML\<close>
 
diff -r 4641f0fdaa59 -r be8c0e039a5e src/HOL/Typerep.thy
--- a/src/HOL/Typerep.thy	Sun Aug 25 12:43:43 2024 +0200
+++ b/src/HOL/Typerep.thy	Sun Aug 25 15:02:19 2024 +0200
@@ -19,6 +19,8 @@
 
 syntax
   "_TYPEREP" :: "type => logic"  ("(1TYPEREP/(1'(_')))")
+syntax_consts
+  "_TYPEREP" \<rightleftharpoons> typerep
 
 parse_translation \<open>
   let