More notation (up to where the open bugs allow me to put it without adding

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

diff --git a/helm/matita/library/Z/z.ma b/helm/matita/library/Z/z.ma
index 9dffcee52c9098e6d4488b443d8ba79f4b5958ec..da249902bc3a251b80c7c0e445a8785b39fb52e5 100644 (file)
--- a/helm/matita/library/Z/z.ma
+++ b/helm/matita/library/Z/z.ma
@@ -123,8 +123,11 @@ definition Zplus :Z \to Z \to Z \def
                 | EQ \Rightarrow OZ
                 | GT \Rightarrow (neg (pred (minus m n)))]     
          | (neg n) \Rightarrow (neg (S (plus 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).
          
-theorem Zplus_z_OZ:  \forall z:Z. eq Z (Zplus z OZ) z.
+theorem Zplus_z_OZ:  \forall z:Z. Zplus z OZ = z.
 intro.elim z.
 simplify.reflexivity.
 simplify.reflexivity.