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