# HG changeset patch
# User wenzelm
# Date 1724924390 -7200
# Node ID f27f66e9adcac05df35fda727a7fc0bc02ef84b7
# Parent  70076ba563d207e0184a23e7782214058b8624ea
more direct notation;

diff -r 70076ba563d2 -r f27f66e9adca src/ZF/List.thy
--- 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"