Library doc adjustments (until page 140)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1655 85f007b7-540e-0410-9357-904b9bb8a0f7

2 files changed, 10 insertions, 7 deletions

diff --git a/theories/Arith/Plus.v b/theories/Arith/Plus.v
index 67121590ee..1b70e1512b 100755
--- a/theories/Arith/Plus.v
+++ b/theories/Arith/Plus.v
@@ -22,8 +22,7 @@ Intros y H ; Elim (plus_n_Sm m y) ; Auto with arith.
 Qed.
 Hints Immediate plus_sym : arith v62.
 
-Lemma plus_Snm_nSm : 
-  (n,m:nat)(plus (S n) m)=(plus n (S m)).
+Lemma plus_Snm_nSm : (n,m:nat)(plus (S n) m)=(plus n (S m)).
 Intros.
 Simpl.
 Rewrite -> (plus_sym n m).
@@ -143,7 +142,8 @@ Proof.
   Intros. Discriminate H.
 Qed.
 
-Lemma plus_is_one : (m,n:nat) (plus m n)=(S O) -> {m=O /\ n=(S O)}+{m=(S O) /\ n=O}.
+Lemma plus_is_one : 
+      (m,n:nat) (plus m n)=(S O) -> {m=O /\ n=(S O)}+{m=(S O) /\ n=O}.
 Proof.
   Destruct m; Auto.
   Destruct n; Auto.
diff --git a/theories/Arith/Wf_nat.v b/theories/Arith/Wf_nat.v
index 2f100ebc52..ff502af946 100755
--- a/theories/Arith/Wf_nat.v
+++ b/theories/Arith/Wf_nat.v
@@ -55,7 +55,8 @@ the ML-like program for [induction_ltof2] is :
 \end{verbatim}
 *)
 
-Theorem induction_ltof1 : (P:A->Set)((x:A)((y:A)(ltof y x)->(P y))->(P x))->(a:A)(P a).
+Theorem induction_ltof1 
+  : (P:A->Set)((x:A)((y:A)(ltof y x)->(P y))->(P x))->(a:A)(P a).
 Proof.
 Intros P F; Cut (n:nat)(a:A)(lt (f a) n)->(P a).
 Intros H a;  Apply (H (S (f a))); Auto with arith.
@@ -68,14 +69,16 @@ Apply Hm.
 Apply lt_le_trans with (f a); Auto with arith.
 Qed. 
 
-Theorem induction_gtof1 : (P:A->Set)((x:A)((y:A)(gtof y x)->(P y))->(P x))->(a:A)(P a).
+Theorem induction_gtof1 
+  : (P:A->Set)((x:A)((y:A)(gtof y x)->(P y))->(P x))->(a:A)(P a).
 Proof induction_ltof1.
 
 Theorem induction_ltof2 
-   : (P:A->Set)((x:A)((y:A)(ltof y x)->(P y))->(P x))->(a:A)(P a).
+  : (P:A->Set)((x:A)((y:A)(ltof y x)->(P y))->(P x))->(a:A)(P a).
 Proof (well_founded_induction A ltof well_founded_ltof).
 
-Theorem induction_gtof2 : (P:A->Set)((x:A)((y:A)(gtof y x)->(P y))->(P x))->(a:A)(P a).
+Theorem induction_gtof2 
+  : (P:A->Set)((x:A)((y:A)(gtof y x)->(P y))->(P x))->(a:A)(P a).
 Proof induction_ltof2.