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