--- a/src/Benchmarks/Quickcheck_Benchmark/Needham_Schroeder_Base.thy Mon Sep 30 23:32:26 2024 +0200
+++ b/src/Benchmarks/Quickcheck_Benchmark/Needham_Schroeder_Base.thy Tue Oct 01 20:39:16 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"
--- a/src/CCL/Set.thy Mon Sep 30 23:32:26 2024 +0200
+++ b/src/CCL/Set.thy Tue Oct 01 20:39:16 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)"
--- a/src/CCL/Term.thy Mon Sep 30 23:32:26 2024 +0200
+++ b/src/CCL/Term.thy Tue Oct 01 20:39:16 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];
--- a/src/CCL/Type.thy Mon Sep 30 23:32:26 2024 +0200
+++ b/src/CCL/Type.thy Tue Oct 01 20:39:16 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)"
--- a/src/Doc/Tutorial/Protocol/Message.thy Mon Sep 30 23:32:26 2024 +0200
+++ b/src/Doc/Tutorial/Protocol/Message.thy Tue Oct 01 20:39:16 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"
--- a/src/FOL/IFOL.thy Mon Sep 30 23:32:26 2024 +0200
+++ b/src/FOL/IFOL.thy Tue Oct 01 20:39:16 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)"
--- a/src/HOL/Auth/Message.thy Mon Sep 30 23:32:26 2024 +0200
+++ b/src/HOL/Auth/Message.thy Tue Oct 01 20:39:16 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"
--- a/src/HOL/Codegenerator_Test/Code_Lazy_Test.thy Mon Sep 30 23:32:26 2024 +0200
+++ b/src/HOL/Codegenerator_Test/Code_Lazy_Test.thy Tue Oct 01 20:39:16 2024 +0200
@@ -25,8 +25,6 @@
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
- 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 Mon Sep 30 23:32:26 2024 +0200
+++ b/src/HOL/Computational_Algebra/Polynomial.thy Tue Oct 01 20:39:16 2024 +0200
@@ -350,8 +350,6 @@
syntax
"_poly" :: "args \<Rightarrow> 'a poly" (\<open>(\<open>indent=2 notation=\<open>mixfix polynomial enumeration\<close>\<close>[:_:])\<close>)
-syntax_consts
- pCons
translations
"[:x, xs:]" \<rightleftharpoons> "CONST pCons x [:xs:]"
"[:x:]" \<rightleftharpoons> "CONST pCons x 0"
--- a/src/HOL/Fun.thy Mon Sep 30 23:32:26 2024 +0200
+++ b/src/HOL/Fun.thy Tue Oct 01 20:39:16 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"
--- a/src/HOL/HOLCF/ConvexPD.thy Mon Sep 30 23:32:26 2024 +0200
+++ b/src/HOL/HOLCF/ConvexPD.thy Tue Oct 01 20:39:16 2024 +0200
@@ -180,8 +180,6 @@
syntax
"_convex_pd" :: "args \<Rightarrow> logic" (\<open>(\<open>indent=1 notation=\<open>mixfix convex_pd enumeration\<close>\<close>{_}\<natural>)\<close>)
-syntax_consts
- convex_add
translations
"{x,xs}\<natural>" == "{x}\<natural> \<union>\<natural> {xs}\<natural>"
"{x}\<natural>" == "CONST convex_unit\<cdot>x"
--- a/src/HOL/HOLCF/IOA/Sequence.thy Mon Sep 30 23:32:26 2024 +0200
+++ b/src/HOL/HOLCF/IOA/Sequence.thy Tue Oct 01 20:39:16 2024 +0200
@@ -72,8 +72,6 @@
syntax
"_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>)
-syntax_consts
- Consq
translations
"[x, xs!]" \<rightleftharpoons> "x \<leadsto> [xs!]"
"[x!]" \<rightleftharpoons> "x\<leadsto>nil"
--- a/src/HOL/HOLCF/LowerPD.thy Mon Sep 30 23:32:26 2024 +0200
+++ b/src/HOL/HOLCF/LowerPD.thy Tue Oct 01 20:39:16 2024 +0200
@@ -135,8 +135,6 @@
syntax
"_lower_pd" :: "args \<Rightarrow> logic" (\<open>(\<open>indent=1 notation=\<open>mixfix lower_pd enumeration\<close>\<close>{_}\<flat>)\<close>)
-syntax_consts
- lower_add
translations
"{x,xs}\<flat>" == "{x}\<flat> \<union>\<flat> {xs}\<flat>"
"{x}\<flat>" == "CONST lower_unit\<cdot>x"
--- a/src/HOL/HOLCF/Sprod.thy Mon Sep 30 23:32:26 2024 +0200
+++ b/src/HOL/HOLCF/Sprod.thy Tue Oct 01 20:39:16 2024 +0200
@@ -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"
--- a/src/HOL/HOLCF/UpperPD.thy Mon Sep 30 23:32:26 2024 +0200
+++ b/src/HOL/HOLCF/UpperPD.thy Tue Oct 01 20:39:16 2024 +0200
@@ -133,8 +133,6 @@
syntax
"_upper_pd" :: "args \<Rightarrow> logic" (\<open>(\<open>indent=1 notation=\<open>mixfix upper_pd enumeration\<close>\<close>{_}\<sharp>)\<close>)
-syntax_consts
- upper_add
translations
"{x,xs}\<sharp>" == "{x}\<sharp> \<union>\<sharp> {xs}\<sharp>"
"{x}\<sharp>" == "CONST upper_unit\<cdot>x"
--- a/src/HOL/Library/FSet.thy Mon Sep 30 23:32:26 2024 +0200
+++ b/src/HOL/Library/FSet.thy Tue Oct 01 20:39:16 2024 +0200
@@ -166,8 +166,6 @@
syntax
"_fset" :: "args => 'a fset" (\<open>(\<open>indent=2 notation=\<open>mixfix finite set enumeration\<close>\<close>{|_|})\<close>)
-syntax_consts
- finsert
translations
"{|x, xs|}" == "CONST finsert x {|xs|}"
"{|x|}" == "CONST finsert x {||}"
--- a/src/HOL/Library/Multiset.thy Mon Sep 30 23:32:26 2024 +0200
+++ b/src/HOL/Library/Multiset.thy Tue Oct 01 20:39:16 2024 +0200
@@ -93,8 +93,6 @@
syntax
"_multiset" :: "args \<Rightarrow> 'a multiset" (\<open>(\<open>indent=2 notation=\<open>mixfix multiset enumeration\<close>\<close>{#_#})\<close>)
-syntax_consts
- add_mset
translations
"{#x, xs#}" == "CONST add_mset x {#xs#}"
"{#x#}" == "CONST add_mset x {#}"
--- a/src/HOL/List.thy Mon Sep 30 23:32:26 2024 +0200
+++ b/src/HOL/List.thy Tue Oct 01 20:39:16 2024 +0200
@@ -47,8 +47,6 @@
syntax
"_list" :: "args => 'a list" (\<open>(\<open>indent=1 notation=\<open>mixfix list enumeration\<close>\<close>[_])\<close>)
-syntax_consts
- Cons
translations
"[x, xs]" == "x#[xs]"
"[x]" == "x#[]"
@@ -137,9 +135,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"
--- a/src/HOL/Metis_Examples/Message.thy Mon Sep 30 23:32:26 2024 +0200
+++ b/src/HOL/Metis_Examples/Message.thy Tue Oct 01 20:39:16 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"
--- a/src/HOL/Product_Type.thy Mon Sep 30 23:32:26 2024 +0200
+++ b/src/HOL/Product_Type.thy Tue Oct 01 20:39:16 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
--- a/src/HOL/Prolog/Test.thy Mon Sep 30 23:32:26 2024 +0200
+++ b/src/HOL/Prolog/Test.thy Tue Oct 01 20:39:16 2024 +0200
@@ -20,8 +20,6 @@
syntax
"_list" :: "args => 'a list" (\<open>(\<open>indent=1 notation=\<open>mixfix list enumeration\<close>\<close>[_])\<close>)
-syntax_consts
- Cons
translations
"[x, xs]" == "x#[xs]"
"[x]" == "x#[]"
--- a/src/HOL/Quotient_Examples/Lift_FSet.thy Mon Sep 30 23:32:26 2024 +0200
+++ b/src/HOL/Quotient_Examples/Lift_FSet.thy Tue Oct 01 20:39:16 2024 +0200
@@ -97,8 +97,6 @@
syntax
"_fset" :: "args => 'a fset" (\<open>(\<open>indent=2 notation=\<open>mixfix finite set enumeration\<close>\<close>{|_|})\<close>)
-syntax_consts
- fcons
translations
"{|x, xs|}" == "CONST fcons x {|xs|}"
"{|x|}" == "CONST fcons x {||}"
--- a/src/HOL/Quotient_Examples/Quotient_FSet.thy Mon Sep 30 23:32:26 2024 +0200
+++ b/src/HOL/Quotient_Examples/Quotient_FSet.thy Tue Oct 01 20:39:16 2024 +0200
@@ -290,8 +290,6 @@
syntax
"_fset" :: "args => 'a fset" (\<open>(\<open>indent=2 notation=\<open>mixfix finite set enumeration\<close>\<close>{|_|})\<close>)
-syntax_consts
- insert_fset
translations
"{|x, xs|}" == "CONST insert_fset x {|xs|}"
"{|x|}" == "CONST insert_fset x {||}"
--- a/src/HOL/SET_Protocol/Message_SET.thy Mon Sep 30 23:32:26 2024 +0200
+++ b/src/HOL/SET_Protocol/Message_SET.thy Tue Oct 01 20:39:16 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"
--- a/src/HOL/Set.thy Mon Sep 30 23:32:26 2024 +0200
+++ b/src/HOL/Set.thy Tue Oct 01 20:39:16 2024 +0200
@@ -145,8 +145,6 @@
syntax
"_Finset" :: "args \<Rightarrow> 'a set" (\<open>(\<open>indent=1 notation=\<open>mixfix set enumeration\<close>\<close>{_})\<close>)
-syntax_consts
- insert
translations
"{x, xs}" \<rightleftharpoons> "CONST insert x {xs}"
"{x}" \<rightleftharpoons> "CONST insert x {}"
--- a/src/HOL/ex/Code_Lazy_Demo.thy Mon Sep 30 23:32:26 2024 +0200
+++ b/src/HOL/ex/Code_Lazy_Demo.thy Tue Oct 01 20:39:16 2024 +0200
@@ -41,8 +41,6 @@
syntax
"_llist" :: "args => 'a list" (\<open>(\<open>indent=1 notation=\<open>mixfix lazy list enumeration\<close>\<close>\<^bold>\<lbrakk>_\<^bold>\<rbrakk>)\<close>)
-syntax_consts
- 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/ZF/Induct/Multiset.thy Mon Sep 30 23:32:26 2024 +0200
+++ b/src/ZF/Induct/Multiset.thy Tue Oct 01 20:39:16 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)"
--- a/src/ZF/List.thy Mon Sep 30 23:32:26 2024 +0200
+++ b/src/ZF/List.thy Tue Oct 01 20:39:16 2024 +0200
@@ -17,8 +17,6 @@
syntax
"_List" :: "is \<Rightarrow> i" (\<open>(\<open>indent=1 notation=\<open>mixfix list enumeration\<close>\<close>[_])\<close>)
-syntax_consts
- Cons
translations
"[x, xs]" == "CONST Cons(x, [xs])"
"[x]" == "CONST Cons(x, [])"
--- a/src/ZF/ZF_Base.thy Mon Sep 30 23:32:26 2024 +0200
+++ b/src/ZF/ZF_Base.thy Tue Oct 01 20:39:16 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)"
@@ -134,8 +128,6 @@
"" :: "i \<Rightarrow> is" (\<open>_\<close>)
"_Enum" :: "[i, is] \<Rightarrow> is" (\<open>_,/ _\<close>)
"_Finset" :: "is \<Rightarrow> i" (\<open>(\<open>indent=1 notation=\<open>mixfix set enumeration\<close>\<close>{_})\<close>)
-syntax_consts
- cons
translations
"{x, xs}" == "CONST cons(x, {xs})"
"{x}" == "CONST cons(x, 0)"
@@ -197,8 +189,6 @@
"" :: "i \<Rightarrow> tuple_args" (\<open>_\<close>)
"_Tuple_args" :: "[i, tuple_args] \<Rightarrow> tuple_args" (\<open>_,/ _\<close>)
"_Tuple" :: "[i, tuple_args] \<Rightarrow> i" (\<open>(\<open>indent=1 notation=\<open>mixfix tuple enumeration\<close>\<close>\<langle>_,/ _\<rangle>)\<close>)
-syntax_consts
- Pair
translations
"\<langle>x, y, z\<rangle>" == "\<langle>x, \<langle>y, z\<rangle>\<rangle>"
"\<langle>x, y\<rangle>" == "CONST Pair(x, y)"
--- a/src/ZF/func.thy Mon Sep 30 23:32:26 2024 +0200
+++ b/src/ZF/func.thy Tue Oct 01 20:39:16 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)"