librarySync - we do not generate the object attributes when we publish the xml

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

diff --git a/matita/library/Z/plus.ma b/matita/library/Z/plus.ma
index 976f6cfb3ce01d379244fc66ec964a99563917d3..2b439b92e273c83d0e9175bd402d32d0fb363b64 100644 (file)
--- a/matita/library/Z/plus.ma
+++ b/matita/library/Z/plus.ma
@@ -299,3 +299,7 @@ rewrite > nat_compare_n_n.
 simplify.apply refl_eq.
 qed.
 
+(* minus *)
+definition Zminus : Z \to Z \to Z \def \lambda x,y:Z. x + (-y).
+
+interpretation "integer minus" 'minus x y = (cic:/matita/Z/plus/Zminus.con x y).