X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fground%2Farith%2Fnat_minus.ma;h=5d3726ca85c53b1dd16a30d5c7891079a3b51098;hb=888840f6b3a71d3d686b53b702d362ab90ab0038;hp=d975ff3bc59cdc6b145519090877d721d9c6f9dc;hpb=19b0a814861157ba05f23877d5cd94059f52c2e8;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/ground/arith/nat_minus.ma b/matita/matita/contribs/lambdadelta/ground/arith/nat_minus.ma
index d975ff3bc..5d3726ca8 100644
--- a/matita/matita/contribs/lambdadelta/ground/arith/nat_minus.ma
+++ b/matita/matita/contribs/lambdadelta/ground/arith/nat_minus.ma
@@ -22,7 +22,7 @@ definition nminus: nat → nat → nat ≝
            λm,n. npred^n m.
 
 interpretation
-  "minus (positive integers)"
+  "minus (non-negative integers)"
   'minus m n = (nminus m n).
 
 (* Basic constructions ******************************************************)