--- 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)"
--- 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))"
--- 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"
--- 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"
--- 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>
--- 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}"
--- 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)"
--- 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)"
--- 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)"
--- 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)"
--- 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"
--- 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"
--- 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"
--- 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)"
--- 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
--- 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}"
--- 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>
--- 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