--- a/src/Doc/Datatypes/Datatypes.thy Wed Aug 28 20:46:45 2024 +0200
+++ b/src/Doc/Datatypes/Datatypes.thy Wed Aug 28 22:54:45 2024 +0200
@@ -453,7 +453,7 @@
Incidentally, this is how the traditional syntax can be set up:
\<close>
- syntax "_list" :: "args \<Rightarrow> 'a list" ("[(_)]")
+ syntax "_list" :: "list_args \<Rightarrow> 'a list" ("[(_)]")
text \<open>\blankline\<close>
--- a/src/Doc/Tutorial/Protocol/Message.thy Wed Aug 28 20:46:45 2024 +0200
+++ b/src/Doc/Tutorial/Protocol/Message.thy Wed Aug 28 22:54:45 2024 +0200
@@ -79,13 +79,16 @@
(*<*)
text\<open>Concrete syntax: messages appear as \<open>\<lbrace>A,B,NA\<rbrace>\<close>, etc...\<close>
+nonterminal mtuple_args
syntax
- "_MTuple" :: "['a, args] \<Rightarrow> 'a * 'b" ("(2\<lbrace>_,/ _\<rbrace>)")
+ "" :: "'a \<Rightarrow> mtuple_args" ("_")
+ "_MTuple_args" :: "'a \<Rightarrow> mtuple_args \<Rightarrow> mtuple_args" ("_,/ _")
+ "_MTuple" :: "['a, mtuple_args] \<Rightarrow> 'a * 'b" ("(2\<lbrace>_,/ _\<rbrace>)")
syntax_consts
- "_MTuple" == MPair
+ "_MTuple_args" "_MTuple" \<rightleftharpoons> MPair
translations
- "\<lbrace>x, y, z\<rbrace>" == "\<lbrace>x, \<lbrace>y, z\<rbrace>\<rbrace>"
- "\<lbrace>x, y\<rbrace>" == "CONST MPair x y"
+ "\<lbrace>x, y, z\<rbrace>" \<rightleftharpoons> "\<lbrace>x, \<lbrace>y, z\<rbrace>\<rbrace>"
+ "\<lbrace>x, y\<rbrace>" \<rightleftharpoons> "CONST MPair x y"
definition keysFor :: "msg set \<Rightarrow> key set" where
--- a/src/HOL/Auth/Message.thy Wed Aug 28 20:46:45 2024 +0200
+++ b/src/HOL/Auth/Message.thy Wed Aug 28 22:54:45 2024 +0200
@@ -49,10 +49,13 @@
text\<open>Concrete syntax: messages appear as \<open>\<lbrace>A,B,NA\<rbrace>\<close>, etc...\<close>
+nonterminal mtuple_args
syntax
- "_MTuple" :: "['a, args] \<Rightarrow> 'a * 'b" ("(2\<lbrace>_,/ _\<rbrace>)")
+ "" :: "'a \<Rightarrow> mtuple_args" ("_")
+ "_MTuple_args" :: "'a \<Rightarrow> mtuple_args \<Rightarrow> mtuple_args" ("_,/ _")
+ "_MTuple" :: "['a, mtuple_args] \<Rightarrow> 'a * 'b" ("(2\<lbrace>_,/ _\<rbrace>)")
syntax_consts
- "_MTuple" \<rightleftharpoons> MPair
+ "_MTuple_args" "_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 Wed Aug 28 20:46:45 2024 +0200
+++ b/src/HOL/Codegenerator_Test/Code_Lazy_Test.thy Wed Aug 28 22:54:45 2024 +0200
@@ -23,8 +23,13 @@
code_lazy_type llist
no_notation lazy_llist ("_")
-syntax "_llist" :: "args => 'a list" ("\<^bold>[(_)\<^bold>]")
-syntax_consts "_llist" == lazy_llist
+nonterminal llist_args
+syntax
+ "" :: "'a \<Rightarrow> llist_args" ("_")
+ "_llist_args" :: "'a \<Rightarrow> llist_args \<Rightarrow> llist_args" ("_,/ _")
+ "_llist" :: "llist_args => 'a list" ("\<^bold>[(_)\<^bold>]")
+syntax_consts
+ "_llist_args" "_llist" == 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 Wed Aug 28 20:46:45 2024 +0200
+++ b/src/HOL/Computational_Algebra/Polynomial.thy Wed Aug 28 22:54:45 2024 +0200
@@ -348,7 +348,13 @@
subsection \<open>List-style syntax for polynomials\<close>
-syntax "_poly" :: "args \<Rightarrow> 'a poly" ("[:(_):]")
+nonterminal poly_args
+syntax
+ "" :: "'a \<Rightarrow> poly_args" ("_")
+ "_poly_args" :: "'a \<Rightarrow> poly_args \<Rightarrow> poly_args" ("_,/ _")
+ "_poly" :: "poly_args \<Rightarrow> 'a poly" ("[:(_):]")
+syntax_consts
+ "_poly_args" "_poly" \<rightleftharpoons> pCons
translations
"[:x, xs:]" \<rightleftharpoons> "CONST pCons x [:xs:]"
"[:x:]" \<rightleftharpoons> "CONST pCons x 0"
--- a/src/HOL/HOLCF/ConvexPD.thy Wed Aug 28 20:46:45 2024 +0200
+++ b/src/HOL/HOLCF/ConvexPD.thy Wed Aug 28 22:54:45 2024 +0200
@@ -178,12 +178,13 @@
(infixl "\<union>\<natural>" 65) where
"xs \<union>\<natural> ys == convex_plus\<cdot>xs\<cdot>ys"
+nonterminal convex_pd_args
syntax
- "_convex_pd" :: "args \<Rightarrow> logic" ("{_}\<natural>")
-
+ "" :: "logic \<Rightarrow> convex_pd_args" ("_")
+ "_convex_pd_args" :: "logic \<Rightarrow> convex_pd_args \<Rightarrow> convex_pd_args" ("_,/ _")
+ "_convex_pd" :: "convex_pd_args \<Rightarrow> logic" ("{_}\<natural>")
syntax_consts
- "_convex_pd" == convex_add
-
+ "_convex_pd_args" "_convex_pd" == 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 Wed Aug 28 20:46:45 2024 +0200
+++ b/src/HOL/HOLCF/IOA/Sequence.thy Wed Aug 28 22:54:45 2024 +0200
@@ -69,9 +69,12 @@
subsection \<open>List enumeration\<close>
+nonterminal llist_args
syntax
- "_totlist" :: "args \<Rightarrow> 'a Seq" ("[(_)!]")
- "_partlist" :: "args \<Rightarrow> 'a Seq" ("[(_)?]")
+ "" :: "'a \<Rightarrow> llist_args" ("_")
+ "_list_args" :: "'a \<Rightarrow> llist_args \<Rightarrow> llist_args" ("_,/ _")
+ "_totlist" :: "llist_args \<Rightarrow> 'a Seq" ("[(_)!]")
+ "_partlist" :: "llist_args \<Rightarrow> 'a Seq" ("[(_)?]")
syntax_consts
"_totlist" "_partlist" \<rightleftharpoons> Consq
translations
--- a/src/HOL/HOLCF/LowerPD.thy Wed Aug 28 20:46:45 2024 +0200
+++ b/src/HOL/HOLCF/LowerPD.thy Wed Aug 28 22:54:45 2024 +0200
@@ -133,12 +133,13 @@
(infixl "\<union>\<flat>" 65) where
"xs \<union>\<flat> ys == lower_plus\<cdot>xs\<cdot>ys"
+nonterminal lower_pd_args
syntax
- "_lower_pd" :: "args \<Rightarrow> logic" ("{_}\<flat>")
-
+ "" :: "logic \<Rightarrow> lower_pd_args" ("_")
+ "_lower_pd_args" :: "logic \<Rightarrow> lower_pd_args \<Rightarrow> lower_pd_args" ("_,/ _")
+ "_lower_pd" :: "lower_pd_args \<Rightarrow> logic" ("{_}\<flat>")
syntax_consts
- "_lower_pd" == lower_add
-
+ "_lower_pd_args" "_lower_pd" == 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 Wed Aug 28 20:46:45 2024 +0200
+++ b/src/HOL/HOLCF/Sprod.thy Wed Aug 28 22:54:45 2024 +0200
@@ -40,8 +40,13 @@
definition ssplit :: "('a \<rightarrow> 'b \<rightarrow> 'c) \<rightarrow> ('a ** 'b) \<rightarrow> 'c"
where "ssplit = (\<Lambda> f p. seq\<cdot>p\<cdot>(f\<cdot>(sfst\<cdot>p)\<cdot>(ssnd\<cdot>p)))"
-syntax "_stuple" :: "[logic, args] \<Rightarrow> logic" ("(1'(:_,/ _:'))")
-syntax_consts "_stuple" \<rightleftharpoons> spair
+nonterminal stuple_args
+syntax
+ "" :: "logic \<Rightarrow> stuple_args" ("_")
+ "_stuple_args" :: "logic \<Rightarrow> stuple_args \<Rightarrow> stuple_args" ("_,/ _")
+ "_stuple" :: "[logic, stuple_args] \<Rightarrow> logic" ("(1'(:_,/ _:'))")
+syntax_consts
+ "_stuple_args" "_stuple" \<rightleftharpoons> spair
translations
"(:x, y, z:)" \<rightleftharpoons> "(:x, (:y, z:):)"
"(:x, y:)" \<rightleftharpoons> "CONST spair\<cdot>x\<cdot>y"
--- a/src/HOL/HOLCF/UpperPD.thy Wed Aug 28 20:46:45 2024 +0200
+++ b/src/HOL/HOLCF/UpperPD.thy Wed Aug 28 22:54:45 2024 +0200
@@ -131,12 +131,13 @@
(infixl "\<union>\<sharp>" 65) where
"xs \<union>\<sharp> ys == upper_plus\<cdot>xs\<cdot>ys"
+nonterminal upper_pd_args
syntax
- "_upper_pd" :: "args \<Rightarrow> logic" ("{_}\<sharp>")
-
+ "" :: "logic \<Rightarrow> upper_pd_args" ("_")
+ "_upper_pd_args" :: "logic \<Rightarrow> upper_pd_args \<Rightarrow> upper_pd_args" ("_,/ _")
+ "_upper_pd" :: "upper_pd_args \<Rightarrow> logic" ("{_}\<sharp>")
syntax_consts
- "_upper_pd" == upper_add
-
+ "_upper_pd_args" "_upper_pd" == 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 Wed Aug 28 20:46:45 2024 +0200
+++ b/src/HOL/Library/FSet.thy Wed Aug 28 22:54:45 2024 +0200
@@ -164,12 +164,13 @@
lift_definition finsert :: "'a \<Rightarrow> 'a fset \<Rightarrow> 'a fset" is insert parametric Lifting_Set.insert_transfer
by simp
+nonterminal fset_args
syntax
- "_insert_fset" :: "args => 'a fset" ("{|(_)|}")
-
+ "" :: "'a \<Rightarrow> fset_args" ("_")
+ "_fset_args" :: "'a \<Rightarrow> fset_args \<Rightarrow> fset_args" ("_,/ _")
+ "_fset" :: "fset_args => 'a fset" ("{|(_)|}")
syntax_consts
- "_insert_fset" == finsert
-
+ "_fset_args" "_fset" == finsert
translations
"{|x, xs|}" == "CONST finsert x {|xs|}"
"{|x|}" == "CONST finsert x {||}"
--- a/src/HOL/Library/Multiset.thy Wed Aug 28 20:46:45 2024 +0200
+++ b/src/HOL/Library/Multiset.thy Wed Aug 28 22:54:45 2024 +0200
@@ -91,10 +91,13 @@
"\<lambda>a M b. if b = a then Suc (M b) else M b"
by (rule add_mset_in_multiset)
+nonterminal multiset_args
syntax
- "_multiset" :: "args \<Rightarrow> 'a multiset" ("{#(_)#}")
+ "" :: "'a \<Rightarrow> multiset_args" ("_")
+ "_multiset_args" :: "'a \<Rightarrow> multiset_args \<Rightarrow> multiset_args" ("_,/ _")
+ "_multiset" :: "multiset_args \<Rightarrow> 'a multiset" ("{#(_)#}")
syntax_consts
- "_multiset" == add_mset
+ "_multiset_args" "_multiset" == add_mset
translations
"{#x, xs#}" == "CONST add_mset x {#xs#}"
"{#x#}" == "CONST add_mset x {#}"
--- a/src/HOL/List.thy Wed Aug 28 20:46:45 2024 +0200
+++ b/src/HOL/List.thy Wed Aug 28 22:54:45 2024 +0200
@@ -42,13 +42,16 @@
lemmas set_simps = list.set (* legacy *)
+
+text \<open>List enumeration\<close>
+
+nonterminal list_args
syntax
- \<comment> \<open>list Enumeration\<close>
- "_list" :: "args => 'a list" ("[(_)]")
-
+ "" :: "'a \<Rightarrow> list_args" ("_")
+ "_list_args" :: "'a \<Rightarrow> list_args \<Rightarrow> list_args" ("_,/ _")
+ "_list" :: "list_args => 'a list" ("[(_)]")
syntax_consts
- "_list" == Cons
-
+ "_list_args" "_list" == Cons
translations
"[x, xs]" == "x#[xs]"
"[x]" == "x#[]"
--- a/src/HOL/Metis_Examples/Message.thy Wed Aug 28 20:46:45 2024 +0200
+++ b/src/HOL/Metis_Examples/Message.thy Wed Aug 28 22:54:45 2024 +0200
@@ -48,13 +48,16 @@
text\<open>Concrete syntax: messages appear as \<open>\<lbrace>A,B,NA\<rbrace>\<close>, etc...\<close>
+nonterminal mtuple_args
syntax
- "_MTuple" :: "['a, args] => 'a * 'b" ("(2\<lbrace>_,/ _\<rbrace>)")
+ "" :: "'a \<Rightarrow> mtuple_args" ("_")
+ "_MTuple_args" :: "'a \<Rightarrow> mtuple_args \<Rightarrow> mtuple_args" ("_,/ _")
+ "_MTuple" :: "['a, mtuple_args] \<Rightarrow> 'a * 'b" ("(2\<lbrace>_,/ _\<rbrace>)")
syntax_consts
- "_MTuple" == MPair
+ "_MTuple_args" "_MTuple" \<rightleftharpoons> MPair
translations
- "\<lbrace>x, y, z\<rbrace>" == "\<lbrace>x, \<lbrace>y, z\<rbrace>\<rbrace>"
- "\<lbrace>x, y\<rbrace>" == "CONST MPair x y"
+ "\<lbrace>x, y, z\<rbrace>" \<rightleftharpoons> "\<lbrace>x, \<lbrace>y, z\<rbrace>\<rbrace>"
+ "\<lbrace>x, y\<rbrace>" \<rightleftharpoons> "CONST MPair x y"
definition HPair :: "[msg,msg] => msg" ("(4Hash[_] /_)" [0, 1000]) where
--- a/src/HOL/Prolog/Test.thy Wed Aug 28 20:46:45 2024 +0200
+++ b/src/HOL/Prolog/Test.thy Wed Aug 28 22:54:45 2024 +0200
@@ -16,13 +16,18 @@
Nil :: "'a list" ("[]")
Cons :: "'a => 'a list => 'a list" (infixr "#" 65)
-syntax
- (* list Enumeration *)
- "_list" :: "args => 'a list" ("[(_)]")
+text \<open>List enumeration\<close>
+nonterminal list_args
+syntax
+ "" :: "'a \<Rightarrow> list_args" ("_")
+ "_list_args" :: "'a \<Rightarrow> list_args \<Rightarrow> list_args" ("_,/ _")
+ "_list" :: "list_args => 'a list" ("[(_)]")
+syntax_consts
+ "_list_args" "_list" == Cons
translations
- "[x, xs]" == "x#[xs]"
- "[x]" == "x#[]"
+ "[x, xs]" == "x#[xs]"
+ "[x]" == "x#[]"
typedecl person
--- a/src/HOL/Quotient_Examples/Lift_FSet.thy Wed Aug 28 20:46:45 2024 +0200
+++ b/src/HOL/Quotient_Examples/Lift_FSet.thy Wed Aug 28 22:54:45 2024 +0200
@@ -95,12 +95,13 @@
end
+nonterminal fset_args
syntax
- "_insert_fset" :: "args => 'a fset" ("{|(_)|}")
-
+ "" :: "'a \<Rightarrow> fset_args" ("_")
+ "_fset_args" :: "'a \<Rightarrow> fset_args \<Rightarrow> fset_args" ("_,/ _")
+ "_fset" :: "fset_args => 'a fset" ("{|(_)|}")
syntax_consts
- "_insert_fset" == fcons
-
+ "_fset_args" "_fset" == fcons
translations
"{|x, xs|}" == "CONST fcons x {|xs|}"
"{|x|}" == "CONST fcons x {||}"
--- a/src/HOL/Quotient_Examples/Quotient_FSet.thy Wed Aug 28 20:46:45 2024 +0200
+++ b/src/HOL/Quotient_Examples/Quotient_FSet.thy Wed Aug 28 22:54:45 2024 +0200
@@ -288,12 +288,13 @@
"insert_fset :: 'a \<Rightarrow> 'a fset \<Rightarrow> 'a fset"
is "Cons" by auto
+nonterminal fset_args
syntax
- "_insert_fset" :: "args => 'a fset" ("{|(_)|}")
-
+ "" :: "'a \<Rightarrow> fset_args" ("_")
+ "_fset_args" :: "'a \<Rightarrow> fset_args \<Rightarrow> fset_args" ("_,/ _")
+ "_fset" :: "fset_args => 'a fset" ("{|(_)|}")
syntax_consts
- "_insert_fset" == insert_fset
-
+ "_fset_args" "_fset" == insert_fset
translations
"{|x, xs|}" == "CONST insert_fset x {|xs|}"
"{|x|}" == "CONST insert_fset x {||}"
--- a/src/HOL/SET_Protocol/Message_SET.thy Wed Aug 28 20:46:45 2024 +0200
+++ b/src/HOL/SET_Protocol/Message_SET.thy Wed Aug 28 22:54:45 2024 +0200
@@ -68,10 +68,13 @@
(*Concrete syntax: messages appear as \<open>\<lbrace>A,B,NA\<rbrace>\<close>, etc...*)
+nonterminal mtuple_args
syntax
- "_MTuple" :: "['a, args] \<Rightarrow> 'a * 'b" ("(2\<lbrace>_,/ _\<rbrace>)")
+ "" :: "'a \<Rightarrow> mtuple_args" ("_")
+ "_MTuple_args" :: "'a \<Rightarrow> mtuple_args \<Rightarrow> mtuple_args" ("_,/ _")
+ "_MTuple" :: "['a, mtuple_args] \<Rightarrow> 'a * 'b" ("(2\<lbrace>_,/ _\<rbrace>)")
syntax_consts
- "_MTuple" == MPair
+ "_MTuple_args" "_MTuple" \<rightleftharpoons> MPair
translations
"\<lbrace>x, y, z\<rbrace>" == "\<lbrace>x, \<lbrace>y, z\<rbrace>\<rbrace>"
"\<lbrace>x, y\<rbrace>" == "CONST MPair x y"
--- a/src/HOL/Set.thy Wed Aug 28 20:46:45 2024 +0200
+++ b/src/HOL/Set.thy Wed Aug 28 22:54:45 2024 +0200
@@ -143,10 +143,13 @@
definition insert :: "'a \<Rightarrow> 'a set \<Rightarrow> 'a set"
where insert_compr: "insert a B = {x. x = a \<or> x \<in> B}"
+nonterminal finset_args
syntax
- "_Finset" :: "args \<Rightarrow> 'a set" ("{(_)}")
+ "" :: "'a \<Rightarrow> finset_args" ("_")
+ "_Finset_args" :: "'a \<Rightarrow> finset_args \<Rightarrow> finset_args" ("_,/ _")
+ "_Finset" :: "finset_args \<Rightarrow> 'a set" ("{(_)}")
syntax_consts
- "_Finset" \<rightleftharpoons> insert
+ "_Finset_args" "_Finset" \<rightleftharpoons> insert
translations
"{x, xs}" \<rightleftharpoons> "CONST insert x {xs}"
"{x}" \<rightleftharpoons> "CONST insert x {}"
--- a/src/HOL/ex/Code_Lazy_Demo.thy Wed Aug 28 20:46:45 2024 +0200
+++ b/src/HOL/ex/Code_Lazy_Demo.thy Wed Aug 28 22:54:45 2024 +0200
@@ -39,8 +39,13 @@
= LNil ("\<^bold>\<lbrakk>\<^bold>\<rbrakk>")
| LCons (lhd: 'a) (ltl: "'a llist") (infixr "###" 65)
-syntax "_llist" :: "args => 'a list" ("\<^bold>\<lbrakk>(_)\<^bold>\<rbrakk>")
-syntax_consts "_llist" == LCons
+nonterminal llist_args
+syntax
+ "" :: "'a \<Rightarrow> llist_args" ("_")
+ "_llist_args" :: "'a \<Rightarrow> llist_args \<Rightarrow> llist_args" ("_,/ _")
+ "_llist" :: "llist_args => 'a list" ("\<^bold>\<lbrakk>(_)\<^bold>\<rbrakk>")
+syntax_consts
+ "_llist_args" "_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>"