From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Wed, 13 Jul 2005 10:15:30 +0000 (+0000)
Subject: removed drop.
X-Git-Tag: pre_notation~21
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=11dc90870a5c1afdb1fb3c62a4098db0666dcc93;p=helm.git

removed drop.
---

diff --git a/helm/matita/library/Z/z.ma b/helm/matita/library/Z/z.ma
index f59d7b369..aa50a0003 100644
--- a/helm/matita/library/Z/z.ma
+++ b/helm/matita/library/Z/z.ma
@@ -310,11 +310,10 @@ qed.
 
 
 theorem associative_Zplus: associative Z Zplus.
-(* change with (\forall x,y,z. eq ?(Zplus (Zplus x y) z) (Zplus x (Zplus y z))).*)
-simplify.
+change with (\forall x,y,z. eq ?(Zplus (Zplus x y) z) (Zplus x (Zplus y z))).
+(* simplify. *) 
 intros.elim x.simplify.reflexivity.
 elim e1.rewrite < (Zpred_Zplus_neg_O (Zplus y z)).
-drop.
 rewrite < (Zpred_Zplus_neg_O y).
 rewrite < Zplus_Zpred.
 reflexivity.