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