X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Flegacy_1%2Fcoq%2Fdefs.ma;h=497403d328dc5b76e0462a651e11c5cb41b4988e;hb=57ae1762497a5f3ea75740e2908e04adb8642cc2;hp=75e58b0364f93ac5077e8fb475a8ce0d70517b29;hpb=e51d01099c08e9945ea093da6fcac353db7ca23c;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/legacy_1/coq/defs.ma b/matita/matita/contribs/lambdadelta/legacy_1/coq/defs.ma
index 75e58b036..497403d32 100644
--- a/matita/matita/contribs/lambdadelta/legacy_1/coq/defs.ma
+++ b/matita/matita/contribs/lambdadelta/legacy_1/coq/defs.ma
@@ -68,12 +68,12 @@ definition pred:
 \def
  \lambda (n: nat).(match n with [O \Rightarrow O | (S u) \Rightarrow u]).
 
-let rec plus (n: nat) on n: nat \to nat \def \lambda (m: nat).(match n with 
-[O \Rightarrow m | (S p) \Rightarrow (S (plus p m))]).
+rec definition plus (n: nat) on n: nat \to nat \def \lambda (m: nat).(match n 
+with [O \Rightarrow m | (S p) \Rightarrow (S (plus p m))]).
 
-let rec minus (n: nat) on n: nat \to nat \def \lambda (m: nat).(match n with 
-[O \Rightarrow O | (S k) \Rightarrow (match m with [O \Rightarrow (S k) | (S 
-l) \Rightarrow (minus k l)])]).
+rec definition minus (n: nat) on n: nat \to nat \def \lambda (m: nat).(match 
+n with [O \Rightarrow O | (S k) \Rightarrow (match m with [O \Rightarrow (S 
+k) | (S l) \Rightarrow (minus k l)])]).
 
 inductive Acc (A: Type[0]) (R: A \to (A \to Prop)): A \to Prop \def
 | Acc_intro: \forall (x: A).(((\forall (y: A).((R y x) \to (Acc A R y)))) \to