milestone update in ground, partial commit

[helm.git] / matita / matita / contribs / lambdadelta / ground / arith / nat_minus.ma

diff --git a/matita/matita/contribs/lambdadelta/ground/arith/nat_minus.ma b/matita/matita/contribs/lambdadelta/ground/arith/nat_minus.ma
index d975ff3bc59cdc6b145519090877d721d9c6f9dc..5d3726ca85c53b1dd16a30d5c7891079a3b51098 100644 (file)
--- 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 ******************************************************)