clarified inner-syntax markup, notably for enumerations: prefer "notation=mixfix" over "entity" via 'syntax_consts' (see also 70076ba563d2);
--- a/NEWS Mon Sep 30 13:00:42 2024 +0200
+++ b/NEWS Mon Sep 30 20:30:59 2024 +0200
@@ -28,14 +28,6 @@
*** HOL ***
-* Enumerations for tuples, sets, lists etc. now use specific grammar
-productions and separate syntax constants: this allows PIDE markup
-(hyperlinks) for the separators (commas). For example, instead of
-generic nonterminal "args" and syntax constant "_args" from Pure, HOL
-lists now use nonterminal "list_args" and syntax constant "_list_args".
-Rare INCOMPATIBILITY for ambitious syntax translations and grammar
-modifications (e.g. via 'no_syntax').
-
* Theory "HOL.Wellfounded":
- Removed lemma wellorder.wfP_less. Use wellorder.wfp_on_less instead.
Minor INCOMPATIBILITIES.
--- a/src/Benchmarks/Quickcheck_Benchmark/Needham_Schroeder_Base.thy Mon Sep 30 13:00:42 2024 +0200
+++ b/src/Benchmarks/Quickcheck_Benchmark/Needham_Schroeder_Base.thy Mon Sep 30 20:30:59 2024 +0200
@@ -27,12 +27,12 @@
| Crypt key msg
syntax
- "_MTuple" :: "['a, args] => 'a * 'b" ("(2\<lbrace>_,/ _\<rbrace>)")
+ "_MTuple" :: "['a, args] \<Rightarrow> 'a * 'b" (\<open>(\<open>indent=2 notation=\<open>mixfix message tuple\<close>\<close>\<lbrace>_,/ _\<rbrace>)\<close>)
syntax_consts
- "_MTuple" == MPair
+ 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"
inductive_set
parts :: "msg set => msg set"
--- a/src/Doc/Datatypes/Datatypes.thy Mon Sep 30 13:00:42 2024 +0200
+++ b/src/Doc/Datatypes/Datatypes.thy Mon Sep 30 20:30:59 2024 +0200
@@ -452,8 +452,11 @@
\noindent
Incidentally, this is how the traditional syntax can be set up:
\<close>
-
- syntax "_list" :: "list_args \<Rightarrow> 'a list" (\<open>[(_)]\<close>)
+(*<*)
+no_syntax
+ "_list" :: "args => 'a list" (\<open>[(\<open>notation=\<open>mixfix list enumeration\<close>\<close>_)]\<close>)
+(*>*)
+ syntax "_list" :: "args \<Rightarrow> 'a list" (\<open>[(_)]\<close>)
text \<open>\blankline\<close>
--- a/src/Doc/Tutorial/Protocol/Message.thy Mon Sep 30 13:00:42 2024 +0200
+++ b/src/Doc/Tutorial/Protocol/Message.thy Mon Sep 30 20:30:59 2024 +0200
@@ -79,13 +79,10 @@
(*<*)
text\<open>Concrete syntax: messages appear as \<open>\<lbrace>A,B,NA\<rbrace>\<close>, etc...\<close>
-nonterminal mtuple_args
syntax
- "" :: "'a \<Rightarrow> mtuple_args" ("_")
- "_MTuple_args" :: "'a \<Rightarrow> mtuple_args \<Rightarrow> mtuple_args" ("_,/ _")
- "_MTuple" :: "['a, mtuple_args] \<Rightarrow> 'a * 'b" ("(2\<lbrace>_,/ _\<rbrace>)")
+ "_MTuple" :: "['a, args] \<Rightarrow> 'a * 'b" ("(\<open>indent=2 notation=\<open>mixfix message tuple\<close>\<close>\<lbrace>_,/ _\<rbrace>)")
syntax_consts
- "_MTuple_args" "_MTuple" \<rightleftharpoons> MPair
+ 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/Auth/Message.thy Mon Sep 30 13:00:42 2024 +0200
+++ b/src/HOL/Auth/Message.thy Mon Sep 30 20:30:59 2024 +0200
@@ -49,13 +49,10 @@
text\<open>Concrete syntax: messages appear as \<open>\<lbrace>A,B,NA\<rbrace>\<close>, etc...\<close>
-nonterminal mtuple_args
syntax
- "" :: "'a \<Rightarrow> mtuple_args" (\<open>_\<close>)
- "_MTuple_args" :: "'a \<Rightarrow> mtuple_args \<Rightarrow> mtuple_args" (\<open>_,/ _\<close>)
- "_MTuple" :: "['a, mtuple_args] \<Rightarrow> 'a * 'b" (\<open>(2\<lbrace>_,/ _\<rbrace>)\<close>)
+ "_MTuple" :: "['a, args] \<Rightarrow> 'a * 'b" (\<open>(\<open>indent=2 notation=\<open>mixfix message tuple\<close>\<close>\<lbrace>_,/ _\<rbrace>)\<close>)
syntax_consts
- "_MTuple_args" "_MTuple" \<rightleftharpoons> MPair
+ 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 13:00:42 2024 +0200
+++ b/src/HOL/Codegenerator_Test/Code_Lazy_Test.thy Mon Sep 30 20:30:59 2024 +0200
@@ -23,13 +23,10 @@
code_lazy_type llist
no_notation lazy_llist (\<open>_\<close>)
-nonterminal llist_args
syntax
- "" :: "'a \<Rightarrow> llist_args" (\<open>_\<close>)
- "_llist_args" :: "'a \<Rightarrow> llist_args \<Rightarrow> llist_args" (\<open>_,/ _\<close>)
- "_llist" :: "llist_args => 'a list" (\<open>\<^bold>[(_)\<^bold>]\<close>)
+ "_llist" :: "args => 'a list" (\<open>\<^bold>[(\<open>notation=\<open>mixfix lazy list enumeration\<close>\<close>_)\<^bold>]\<close>)
syntax_consts
- "_llist_args" "_llist" == lazy_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 Mon Sep 30 13:00:42 2024 +0200
+++ b/src/HOL/Computational_Algebra/Polynomial.thy Mon Sep 30 20:30:59 2024 +0200
@@ -348,13 +348,10 @@
subsection \<open>List-style syntax for polynomials\<close>
-nonterminal poly_args
syntax
- "" :: "'a \<Rightarrow> poly_args" (\<open>_\<close>)
- "_poly_args" :: "'a \<Rightarrow> poly_args \<Rightarrow> poly_args" (\<open>_,/ _\<close>)
- "_poly" :: "poly_args \<Rightarrow> 'a poly" (\<open>[:(_):]\<close>)
+ "_poly" :: "args \<Rightarrow> 'a poly" (\<open>[:(\<open>notation=\<open>mixfix polynomial enumeration\<close>\<close>_):]\<close>)
syntax_consts
- "_poly_args" "_poly" \<rightleftharpoons> pCons
+ pCons
translations
"[:x, xs:]" \<rightleftharpoons> "CONST pCons x [:xs:]"
"[:x:]" \<rightleftharpoons> "CONST pCons x 0"
--- a/src/HOL/HOLCF/IOA/Sequence.thy Mon Sep 30 13:00:42 2024 +0200
+++ b/src/HOL/HOLCF/IOA/Sequence.thy Mon Sep 30 20:30:59 2024 +0200
@@ -69,14 +69,11 @@
subsection \<open>List enumeration\<close>
-nonterminal llist_args
syntax
- "" :: "'a \<Rightarrow> llist_args" (\<open>_\<close>)
- "_list_args" :: "'a \<Rightarrow> llist_args \<Rightarrow> llist_args" (\<open>_,/ _\<close>)
- "_totlist" :: "llist_args \<Rightarrow> 'a Seq" (\<open>[(_)!]\<close>)
- "_partlist" :: "llist_args \<Rightarrow> 'a Seq" (\<open>[(_)?]\<close>)
+ "_totlist" :: "args \<Rightarrow> 'a Seq" (\<open>[(\<open>notation=\<open>mixfix total list enumeration\<close>\<close>_)!]\<close>)
+ "_partlist" :: "args \<Rightarrow> 'a Seq" (\<open>[(\<open>notation=\<open>mixfix partial list enumeration\<close>\<close>_)?]\<close>)
syntax_consts
- "_totlist" "_partlist" \<rightleftharpoons> Consq
+ Consq
translations
"[x, xs!]" \<rightleftharpoons> "x \<leadsto> [xs!]"
"[x!]" \<rightleftharpoons> "x\<leadsto>nil"
--- a/src/HOL/HOLCF/Sprod.thy Mon Sep 30 13:00:42 2024 +0200
+++ b/src/HOL/HOLCF/Sprod.thy Mon Sep 30 20:30:59 2024 +0200
@@ -40,13 +40,10 @@
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)))"
-nonterminal stuple_args
syntax
- "" :: "logic \<Rightarrow> stuple_args" (\<open>_\<close>)
- "_stuple_args" :: "logic \<Rightarrow> stuple_args \<Rightarrow> stuple_args" (\<open>_,/ _\<close>)
- "_stuple" :: "[logic, stuple_args] \<Rightarrow> logic" (\<open>(1'(:_,/ _:'))\<close>)
+ "_stuple" :: "[logic, args] \<Rightarrow> logic" (\<open>(\<open>indent=1 notation=\<open>mixfix strict tuple\<close>\<close>'(:_,/ _:'))\<close>)
syntax_consts
- "_stuple_args" "_stuple" \<rightleftharpoons> spair
+ spair
translations
"(:x, y, z:)" \<rightleftharpoons> "(:x, (:y, z:):)"
"(:x, y:)" \<rightleftharpoons> "CONST spair\<cdot>x\<cdot>y"
--- a/src/HOL/Library/FSet.thy Mon Sep 30 13:00:42 2024 +0200
+++ b/src/HOL/Library/FSet.thy Mon Sep 30 20:30:59 2024 +0200
@@ -164,13 +164,10 @@
lift_definition finsert :: "'a \<Rightarrow> 'a fset \<Rightarrow> 'a fset" is insert parametric Lifting_Set.insert_transfer
by simp
-nonterminal fset_args
syntax
- "" :: "'a \<Rightarrow> fset_args" (\<open>_\<close>)
- "_fset_args" :: "'a \<Rightarrow> fset_args \<Rightarrow> fset_args" (\<open>_,/ _\<close>)
- "_fset" :: "fset_args => 'a fset" (\<open>{|(_)|}\<close>)
+ "_fset" :: "args => 'a fset" (\<open>{|(\<open>notation=\<open>mixfix finite set enumeration\<close>\<close>_)|}\<close>)
syntax_consts
- "_fset_args" "_fset" == finsert
+ finsert
translations
"{|x, xs|}" == "CONST finsert x {|xs|}"
"{|x|}" == "CONST finsert x {||}"
--- a/src/HOL/Library/Multiset.thy Mon Sep 30 13:00:42 2024 +0200
+++ b/src/HOL/Library/Multiset.thy Mon Sep 30 20:30:59 2024 +0200
@@ -91,13 +91,10 @@
"\<lambda>a M b. if b = a then Suc (M b) else M b"
by (rule add_mset_in_multiset)
-nonterminal multiset_args
syntax
- "" :: "'a \<Rightarrow> multiset_args" (\<open>_\<close>)
- "_multiset_args" :: "'a \<Rightarrow> multiset_args \<Rightarrow> multiset_args" (\<open>_,/ _\<close>)
- "_multiset" :: "multiset_args \<Rightarrow> 'a multiset" (\<open>{#(_)#}\<close>)
+ "_multiset" :: "args \<Rightarrow> 'a multiset" (\<open>{#(\<open>notation=\<open>mixfix multiset enumeration\<close>\<close>_)#}\<close>)
syntax_consts
- "_multiset_args" "_multiset" == add_mset
+ add_mset
translations
"{#x, xs#}" == "CONST add_mset x {#xs#}"
"{#x#}" == "CONST add_mset x {#}"
--- a/src/HOL/List.thy Mon Sep 30 13:00:42 2024 +0200
+++ b/src/HOL/List.thy Mon Sep 30 20:30:59 2024 +0200
@@ -45,13 +45,10 @@
text \<open>List enumeration\<close>
-nonterminal list_args
syntax
- "" :: "'a \<Rightarrow> list_args" (\<open>_\<close>)
- "_list_args" :: "'a \<Rightarrow> list_args \<Rightarrow> list_args" (\<open>_,/ _\<close>)
- "_list" :: "list_args => 'a list" (\<open>[(_)]\<close>)
+ "_list" :: "args => 'a list" (\<open>[(\<open>notation=\<open>mixfix list enumeration\<close>\<close>_)]\<close>)
syntax_consts
- "_list_args" "_list" == Cons
+ Cons
translations
"[x, xs]" == "x#[xs]"
"[x]" == "x#[]"
--- a/src/HOL/Metis_Examples/Message.thy Mon Sep 30 13:00:42 2024 +0200
+++ b/src/HOL/Metis_Examples/Message.thy Mon Sep 30 20:30:59 2024 +0200
@@ -48,13 +48,10 @@
text\<open>Concrete syntax: messages appear as \<open>\<lbrace>A,B,NA\<rbrace>\<close>, etc...\<close>
-nonterminal mtuple_args
syntax
- "" :: "'a \<Rightarrow> mtuple_args" (\<open>_\<close>)
- "_MTuple_args" :: "'a \<Rightarrow> mtuple_args \<Rightarrow> mtuple_args" (\<open>_,/ _\<close>)
- "_MTuple" :: "['a, mtuple_args] \<Rightarrow> 'a * 'b" (\<open>(2\<lbrace>_,/ _\<rbrace>)\<close>)
+ "_MTuple" :: "['a, args] \<Rightarrow> 'a * 'b" (\<open>(\<open>indent=2 notation=\<open>mixfix message tuple\<close>\<close>\<lbrace>_,/ _\<rbrace>)\<close>)
syntax_consts
- "_MTuple_args" "_MTuple" \<rightleftharpoons> MPair
+ 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/Prolog/Test.thy Mon Sep 30 13:00:42 2024 +0200
+++ b/src/HOL/Prolog/Test.thy Mon Sep 30 20:30:59 2024 +0200
@@ -18,13 +18,10 @@
text \<open>List enumeration\<close>
-nonterminal list_args
syntax
- "" :: "'a \<Rightarrow> list_args" (\<open>_\<close>)
- "_list_args" :: "'a \<Rightarrow> list_args \<Rightarrow> list_args" (\<open>_,/ _\<close>)
- "_list" :: "list_args => 'a list" (\<open>[(_)]\<close>)
+ "_list" :: "args => 'a list" (\<open>[(\<open>notation=\<open>mixfix list enumeration\<close>\<close>_)]\<close>)
syntax_consts
- "_list_args" "_list" == Cons
+ Cons
translations
"[x, xs]" == "x#[xs]"
"[x]" == "x#[]"
--- a/src/HOL/Quotient_Examples/Lift_FSet.thy Mon Sep 30 13:00:42 2024 +0200
+++ b/src/HOL/Quotient_Examples/Lift_FSet.thy Mon Sep 30 20:30:59 2024 +0200
@@ -95,13 +95,10 @@
end
-nonterminal fset_args
syntax
- "" :: "'a \<Rightarrow> fset_args" (\<open>_\<close>)
- "_fset_args" :: "'a \<Rightarrow> fset_args \<Rightarrow> fset_args" (\<open>_,/ _\<close>)
- "_fset" :: "fset_args => 'a fset" (\<open>{|(_)|}\<close>)
+ "_fset" :: "args => 'a fset" (\<open>{|(\<open>notation=\<open>mixfix finite set enumeration\<close>\<close>_)|}\<close>)
syntax_consts
- "_fset_args" "_fset" == fcons
+ fcons
translations
"{|x, xs|}" == "CONST fcons x {|xs|}"
"{|x|}" == "CONST fcons x {||}"
--- a/src/HOL/Quotient_Examples/Quotient_FSet.thy Mon Sep 30 13:00:42 2024 +0200
+++ b/src/HOL/Quotient_Examples/Quotient_FSet.thy Mon Sep 30 20:30:59 2024 +0200
@@ -288,13 +288,10 @@
"insert_fset :: 'a \<Rightarrow> 'a fset \<Rightarrow> 'a fset"
is "Cons" by auto
-nonterminal fset_args
syntax
- "" :: "'a \<Rightarrow> fset_args" (\<open>_\<close>)
- "_fset_args" :: "'a \<Rightarrow> fset_args \<Rightarrow> fset_args" (\<open>_,/ _\<close>)
- "_fset" :: "fset_args => 'a fset" (\<open>{|(_)|}\<close>)
+ "_fset" :: "args => 'a fset" (\<open>{|(\<open>notation=\<open>mixfix finite set enumeration\<close>\<close>_)|}\<close>)
syntax_consts
- "_fset_args" "_fset" == insert_fset
+ 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 13:00:42 2024 +0200
+++ b/src/HOL/SET_Protocol/Message_SET.thy Mon Sep 30 20:30:59 2024 +0200
@@ -68,16 +68,13 @@
(*Concrete syntax: messages appear as \<open>\<lbrace>A,B,NA\<rbrace>\<close>, etc...*)
-nonterminal mtuple_args
syntax
- "" :: "'a \<Rightarrow> mtuple_args" (\<open>_\<close>)
- "_MTuple_args" :: "'a \<Rightarrow> mtuple_args \<Rightarrow> mtuple_args" (\<open>_,/ _\<close>)
- "_MTuple" :: "['a, mtuple_args] \<Rightarrow> 'a * 'b" (\<open>(2\<lbrace>_,/ _\<rbrace>)\<close>)
+ "_MTuple" :: "['a, args] \<Rightarrow> 'a * 'b" (\<open>(\<open>indent=2 notation=\<open>mixfix message tuple\<close>\<close>\<lbrace>_,/ _\<rbrace>)\<close>)
syntax_consts
- "_MTuple_args" "_MTuple" \<rightleftharpoons> MPair
+ 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 nat_of_agent :: "agent \<Rightarrow> nat" where
--- a/src/HOL/Set.thy Mon Sep 30 13:00:42 2024 +0200
+++ b/src/HOL/Set.thy Mon Sep 30 20:30:59 2024 +0200
@@ -143,13 +143,10 @@
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
- "" :: "'a \<Rightarrow> finset_args" (\<open>_\<close>)
- "_Finset_args" :: "'a \<Rightarrow> finset_args \<Rightarrow> finset_args" (\<open>_,/ _\<close>)
- "_Finset" :: "finset_args \<Rightarrow> 'a set" (\<open>{(_)}\<close>)
+ "_Finset" :: "args \<Rightarrow> 'a set" (\<open>{(\<open>notation=\<open>mixfix set enumeration\<close>\<close>_)}\<close>)
syntax_consts
- "_Finset_args" "_Finset" \<rightleftharpoons> insert
+ insert
translations
"{x, xs}" \<rightleftharpoons> "CONST insert x {xs}"
"{x}" \<rightleftharpoons> "CONST insert x {}"
--- a/src/HOL/Tools/string_syntax.ML Mon Sep 30 13:00:42 2024 +0200
+++ b/src/HOL/Tools/string_syntax.ML Mon Sep 30 20:30:59 2024 +0200
@@ -123,7 +123,7 @@
fun list_ast_tr' [args] =
Ast.Appl [Ast.Constant \<^syntax_const>\<open>_String\<close>,
- (mk_string_ast o maps dest_char_ast o Ast.unfold_ast \<^syntax_const>\<open>_list_args\<close>) args]
+ (mk_string_ast o maps dest_char_ast o Ast.unfold_ast \<^syntax_const>\<open>_args\<close>) args]
| list_ast_tr' _ = raise Match;
--- a/src/HOL/ex/Code_Lazy_Demo.thy Mon Sep 30 13:00:42 2024 +0200
+++ b/src/HOL/ex/Code_Lazy_Demo.thy Mon Sep 30 20:30:59 2024 +0200
@@ -39,13 +39,10 @@
= LNil (\<open>\<^bold>\<lbrakk>\<^bold>\<rbrakk>\<close>)
| LCons (lhd: 'a) (ltl: "'a llist") (infixr \<open>###\<close> 65)
-nonterminal llist_args
syntax
- "" :: "'a \<Rightarrow> llist_args" (\<open>_\<close>)
- "_llist_args" :: "'a \<Rightarrow> llist_args \<Rightarrow> llist_args" (\<open>_,/ _\<close>)
- "_llist" :: "llist_args => 'a list" (\<open>\<^bold>\<lbrakk>(_)\<^bold>\<rbrakk>\<close>)
+ "_llist" :: "args => 'a list" (\<open>\<^bold>\<lbrakk>(\<open>notation=\<open>mixfix lazy list enumeration\<close>\<close>_)\<^bold>\<rbrakk>\<close>)
syntax_consts
- "_llist_args" "_llist" == LCons
+ 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/List.thy Mon Sep 30 13:00:42 2024 +0200
+++ b/src/ZF/List.thy Mon Sep 30 20:30:59 2024 +0200
@@ -15,11 +15,8 @@
notation Nil (\<open>[]\<close>)
-nonterminal list_args
syntax
- "" :: "i \<Rightarrow> list_args" (\<open>_\<close>)
- "_List_args" :: "[i, list_args] \<Rightarrow> list_args" (\<open>_,/ _\<close>)
- "_List" :: "list_args \<Rightarrow> i" (\<open>[(\<open>notation=\<open>mixfix list enumeration\<close>\<close>_)]\<close>)
+ "_List" :: "is \<Rightarrow> i" (\<open>[(\<open>notation=\<open>mixfix list enumeration\<close>\<close>_)]\<close>)
syntax_consts
Cons
translations
--- a/src/ZF/ZF_Base.thy Mon Sep 30 13:00:42 2024 +0200
+++ b/src/ZF/ZF_Base.thy Mon Sep 30 20:30:59 2024 +0200
@@ -129,11 +129,11 @@
definition succ :: "i \<Rightarrow> i"
where "succ(i) \<equiv> cons(i, i)"
-nonterminal "finset_args"
+nonterminal "is"
syntax
- "" :: "i \<Rightarrow> finset_args" (\<open>_\<close>)
- "_Finset_args" :: "[i, finset_args] \<Rightarrow> finset_args" (\<open>_,/ _\<close>)
- "_Finset" :: "finset_args \<Rightarrow> i" (\<open>{(\<open>notation=\<open>mixfix set enumeration\<close>\<close>_)}\<close>)
+ "" :: "i \<Rightarrow> is" (\<open>_\<close>)
+ "_Enum" :: "[i, is] \<Rightarrow> is" (\<open>_,/ _\<close>)
+ "_Finset" :: "is \<Rightarrow> i" (\<open>{(\<open>notation=\<open>mixfix set enumeration\<close>\<close>_)}\<close>)
syntax_consts
cons
translations