arithmetics for λδ

[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 8129ad55c7b92e0182e6fc5e2fc9e2407b4e218d..7884355703bf90c61dbf275e3b6ac6595e18ff19 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 (positive integers)"
   'minus m n = (nminus m n).
 
 (* Basic rewrites ***********************************************************)