removed debug saving of "foo.conf.xml"

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

diff --git a/helm/matita/library/Z/plus.ma b/helm/matita/library/Z/plus.ma
index b89f291fbb918684cb595dbd54b5d423259e7e23..c1db18b18d949b5573cb93829bb8f3c721cad605 100644 (file)
--- a/helm/matita/library/Z/plus.ma
+++ b/helm/matita/library/Z/plus.ma
@@ -29,7 +29,7 @@ definition Zplus :Z \to Z \to Z \def
               match nat_compare m n with
                 [ LT \Rightarrow (neg (pred (n-m)))
                 | EQ \Rightarrow OZ
-                | GT \Rightarrow (pos (pred (m-n)))]]
+                | GT \Rightarrow (pos (pred (m-n)))] ]
     | (neg m) \Rightarrow
         match y with
          [ OZ \Rightarrow x
@@ -38,7 +38,7 @@ definition Zplus :Z \to Z \to Z \def
                 [ LT \Rightarrow (pos (pred (n-m)))
                 | EQ \Rightarrow OZ
                 | GT \Rightarrow (neg (pred (m-n)))]     
-         | (neg n) \Rightarrow (neg (pred ((S m)+(S n))))]].
+         | (neg n) \Rightarrow (neg (pred ((S m)+(S n))))] ].
 
 (*CSC: the URI must disappear: there is a bug now *)
 interpretation "integer plus" 'plus x y = (cic:/matita/Z/plus/Zplus.con x y).
@@ -169,10 +169,10 @@ elim H.reflexivity.
 qed.
 
 theorem Zplus_Zsucc_neg_neg : 
-\forall n,m. (Zsucc (neg n))+(neg m) = Zsucc ((neg n)+(neg m)).
+\forall n,m. Zsucc (neg n) + neg m = Zsucc (neg n + neg m).
 intros.
 apply nat_elim2
-(\lambda n,m. ((Zsucc (neg n))+(neg m)) = Zsucc ((neg n)+(neg m))).intro.
+(\lambda n,m. Zsucc (neg n) + neg m = Zsucc (neg n + neg m)).intro.
 intros.elim n1.
 simplify. reflexivity.
 elim n2.simplify. reflexivity.
@@ -189,7 +189,7 @@ theorem Zplus_Zsucc_neg_pos:
 \forall n,m. Zsucc (neg n)+(pos m) = Zsucc ((neg n)+(pos m)).
 intros.
 apply nat_elim2
-(\lambda n,m. (Zsucc (neg n))+(pos m) = Zsucc ((neg n)+(pos m))).
+(\lambda n,m. Zsucc (neg n) + (pos m) = Zsucc (neg n + pos m)).
 intros.elim n1.
 simplify. reflexivity.
 elim n2.simplify. reflexivity.