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