New version.

[helm.git] / helm / software / matita / library / Z / plus.ma

diff --git a/helm/software/matita/library/Z/plus.ma b/helm/software/matita/library/Z/plus.ma
index cd565124589d1e20dbac077a384e1aac6fa06125..8fdeff3bcba158a35793a74a10a0795aa59ec59d 100644 (file)
--- a/helm/software/matita/library/Z/plus.ma
+++ b/helm/software/matita/library/Z/plus.ma
@@ -12,8 +12,6 @@
 (*                                                                        *)
 (**************************************************************************)
 
-set "baseuri" "cic:/matita/Z/plus".
-
 include "Z/z.ma".
 include "nat/minus.ma".
 
@@ -308,7 +306,6 @@ intro.simplify.intros (z y).
 rewrite < Zplus_z_OZ.
 rewrite < (Zplus_z_OZ y).
 rewrite < (Zplus_Zopp x).
-rewrite < (Zplus_Zopp x).
 rewrite < assoc_Zplus.
 rewrite < assoc_Zplus.
 apply eq_f2