--- 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)"
--- 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];
--- 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)"
--- 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)"
--- 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)"
--- 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)"
--- 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)"
--- 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)"
--- 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"
--- 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>]"
--- 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"
--- 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"
--- 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"
--- 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"
--- 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)"
--- 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 {||}"
--- 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 {#}"
--- 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"
--- 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"
--- 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)"
--- 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#[]"
--- 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 {||}"
--- 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 {||}"
--- 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"
--- 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"
--- 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 {}"
--- 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
--- 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>"
--- 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)"
--- 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),
--- 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)"
--- 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)"
--- 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)"