From: Stefano Zacchiroli <zack@upsilon.cc>
Date: Thu, 29 Sep 2005 14:56:55 +0000 (+0000)
Subject: moved a (commented) test in a handier position
X-Git-Tag: V_0_7_2_3~274
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=77ad7d412890919298a21903dd4884359cc4f6cd;p=helm.git

moved a (commented) test in a handier position
---

diff --git a/helm/matita/library/list/list.ma b/helm/matita/library/list/list.ma
index 1973dadab..72637c357 100644
--- a/helm/matita/library/list/list.ma
+++ b/helm/matita/library/list/list.ma
@@ -36,6 +36,8 @@ interpretation "nil" 'nil = (cic:/matita/list/list.ind#xpointer(1/1/1) _).
 interpretation "cons" 'cons hd tl =
   (cic:/matita/list/list.ind#xpointer(1/1/2) _ hd tl).
 
+(* theorem test_notation: [O; S O; S (S O)] = O :: S O :: S (S O) :: []. *)
+
 theorem nil_cons:
   \forall A:Set.\forall l:list A.\forall a:A.
     a::l <> [].