From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Thu, 28 Jul 2005 09:00:22 +0000 (+0000)
Subject: More notation.
X-Git-Tag: V_0_7_2~29
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=f8404e07a6b8649e85bf7a4f812a382cd3a37fca;p=helm.git

More notation.
---

diff --git a/helm/matita/library/Z/z.ma b/helm/matita/library/Z/z.ma
index 118cdd55e..d3bc2ee25 100644
--- a/helm/matita/library/Z/z.ma
+++ b/helm/matita/library/Z/z.ma
@@ -108,21 +108,21 @@ definition Zplus :Z \to Z \to Z \def
     | (pos m) \Rightarrow
         match y with
          [ OZ \Rightarrow x
-         | (pos n) \Rightarrow (pos (S (plus m n)))
+         | (pos n) \Rightarrow (pos (S (m+n)))
          | (neg n) \Rightarrow 
               match nat_compare m n with
-                [ LT \Rightarrow (neg (pred (minus n m)))
+                [ LT \Rightarrow (neg (pred (n-m)))
                 | EQ \Rightarrow OZ
-                | GT \Rightarrow (pos (pred (minus m n)))]]
+                | GT \Rightarrow (pos (pred (m-n)))]]
     | (neg m) \Rightarrow
         match y with
          [ OZ \Rightarrow x
          | (pos n) \Rightarrow 
               match nat_compare m n with
-                [ LT \Rightarrow (pos (pred (minus n m)))
+                [ LT \Rightarrow (pos (pred (n-m)))
                 | EQ \Rightarrow OZ
-                | GT \Rightarrow (neg (pred (minus m n)))]     
-         | (neg n) \Rightarrow (neg (S (plus m n)))]].
+                | GT \Rightarrow (neg (pred (m-n)))]     
+         | (neg n) \Rightarrow (neg (S (m+n)))]].
 
 (*CSC: the URI must disappear: there is a bug now *)
 interpretation "integer plus" 'plus x y = (cic:/matita/Z/z/Zplus.con x y).