--- a/src/ZF/List.thy Wed Aug 28 22:54:45 2024 +0200
+++ b/src/ZF/List.thy Thu Aug 29 11:39:50 2024 +0200
@@ -13,15 +13,14 @@
datatype
"list(A)" = Nil | Cons ("a \<in> A", "l \<in> list(A)")
+notation Nil (\<open>[]\<close>)
syntax
- "_Nil" :: i (\<open>[]\<close>)
"_List" :: "is \<Rightarrow> i" (\<open>[(_)]\<close>)
syntax_consts "_List" \<rightleftharpoons> Cons
translations
"[x, xs]" == "CONST Cons(x, [xs])"
"[x]" == "CONST Cons(x, [])"
- "[]" == "CONST Nil"
consts
length :: "i\<Rightarrow>i"