X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fng_assembly%2Ffreescale%2Fnat.ma;h=4753b4cac745c482654b4547ed63bae7c15bfe64;hb=633b66b935bbc2c38a5abc2be958359335123258;hp=aacc7b1dd26f3d0d398751ee25ba661ccaa854e7;hpb=a687cf5e3e9ae6fb6ead058c4a191002f21fa951;p=helm.git

diff --git a/helm/software/matita/contribs/ng_assembly/freescale/nat.ma b/helm/software/matita/contribs/ng_assembly/freescale/nat.ma
index aacc7b1dd..4753b4cac 100755
--- a/helm/software/matita/contribs/ng_assembly/freescale/nat.ma
+++ b/helm/software/matita/contribs/ng_assembly/freescale/nat.ma
@@ -37,15 +37,6 @@ default "natural numbers" cic:/matita/freescale/nat/nat.ind.
 
 alias num (instance 0) = "natural number".
 
-nlet rec nat_ind (P:nat → Prop) (p:P O) (f:Πn:nat.P n → P (S n)) (n:nat) on n : P n ≝
- match n with [ O ⇒ p | S (n1:nat) ⇒ f n1 (nat_ind P p f n1) ].
-
-nlet rec nat_rec (P:nat → Set) (p:P O) (f:Πn:nat.P n → P (S n)) (n:nat) on n : P n ≝
- match n with [ O ⇒ p | S (n1:nat) ⇒ f n1 (nat_rec P p f n1) ].
-
-nlet rec nat_rect (P:nat → Type) (p:P O) (f:Πn:nat.P n → P (S n)) (n:nat) on n : P n ≝
- match n with [ O ⇒ p | S (n1:nat) ⇒ f n1 (nat_rect P p f n1) ].
-
 nlet rec eq_nat (n1,n2:nat) on n1 ≝
  match n1 with
   [ O ⇒ match n2 with [ O ⇒ true | S _ ⇒ false ]