From: Stefano Zacchiroli <zack@upsilon.cc>
Date: Thu, 26 Jan 2006 17:51:06 +0000 (+0000)
Subject: indentation
X-Git-Tag: make_still_working~7752
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=a877debee863033e33a0f7d497e253ad3b076477;p=helm.git

indentation
---

diff --git a/helm/matita/library/nat/nat.ma b/helm/matita/library/nat/nat.ma
index 0156a98ca..b600072c6 100644
--- a/helm/matita/library/nat/nat.ma
+++ b/helm/matita/library/nat/nat.ma
@@ -83,9 +83,10 @@ qed.
 
 theorem nat_elim2 :
  \forall R:nat \to nat \to Prop.
-  (\forall n:nat. R O n) \to 
-  (\forall n:nat. R (S n) O) \to 
-  (\forall n,m:nat. R n m \to R (S n) (S m)) \to \forall n,m:nat. R n m.
+  (\forall n:nat. R O n) 
+  \to (\forall n:nat. R (S n) O) 
+  \to (\forall n,m:nat. R n m \to R (S n) (S m))
+  \to \forall n,m:nat. R n m.
 intros 5;elim n 
   [ apply H
   | apply (nat_case m)