--- a/src/ZF/List.thy Sun Sep 29 21:40:37 2024 +0200
+++ b/src/ZF/List.thy Sun Sep 29 21:57:47 2024 +0200
@@ -19,9 +19,9 @@
syntax
"" :: "i \<Rightarrow> list_args" (\<open>_\<close>)
"_List_args" :: "[i, list_args] \<Rightarrow> list_args" (\<open>_,/ _\<close>)
- "_List" :: "list_args \<Rightarrow> i" (\<open>[(_)]\<close>)
+ "_List" :: "list_args \<Rightarrow> i" (\<open>[(\<open>notation=\<open>mixfix list enumeration\<close>\<close>_)]\<close>)
syntax_consts
- "_List_args" "_List" \<rightleftharpoons> Cons
+ Cons
translations
"[x, xs]" == "CONST Cons(x, [xs])"
"[x]" == "CONST Cons(x, [])"