X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fground%2Farith%2Fpnat_plus.ma;h=e6db03ac46b8cccce12764f84693c9a8e461dc74;hb=68e028d053806177e218ee1a5f8778d3011bef83;hp=eead7943bb2a50d4859b90c3cb6ff2aad0719f63;hpb=df7a2aa19e98dc28e7f22129275a175cead49e2d;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/ground/arith/pnat_plus.ma b/matita/matita/contribs/lambdadelta/ground/arith/pnat_plus.ma
index eead7943b..e6db03ac4 100644
--- a/matita/matita/contribs/lambdadelta/ground/arith/pnat_plus.ma
+++ b/matita/matita/contribs/lambdadelta/ground/arith/pnat_plus.ma
@@ -14,13 +14,13 @@
 
 include "ground/arith/pnat_iter.ma".
 
-(* POSITIVE INTEGERS ********************************************************)
+(* ADDITION FOR POSITIVE INTEGERS *******************************************)
 
 definition pplus: pnat → pnat → pnat ≝
            λp,q. psucc^q p.
 
 interpretation
-  "plus (positive integers"
+  "plus (positive integers)"
   'plus p q = (pplus p q).
 
 (* Basic rewrites ***********************************************************)
@@ -31,7 +31,7 @@ lemma pplus_one_dx (p): ↑p = p + 𝟏.
 lemma pplus_succ_dx (p) (q): ↑(p+q) = p + ↑q.
 // qed.
 
-(* Semigroup properties *****************************************************)
+(* Advanced reweites (semigroup properties) *********************************)
 
 lemma pplus_succ_sn (p) (q): ↑(p+q) = ↑p + q.
 #p #q @(piter_appl … psucc)