Library doc adjustments (until page 140)

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

1 files changed, 19 insertions, 10 deletions

diff --git a/theories/IntMap/Addr.v b/theories/IntMap/Addr.v
index debaed16cf..026b0ef16d 100644
--- a/theories/IntMap/Addr.v
+++ b/theories/IntMap/Addr.v
@@ -7,7 +7,7 @@
 (***********************************************************************)
 (*i 	$Id$	 i*)
 
-(*s Representation of adresses by [positive] the type of binary numbers *)
+(*s Representation of adresses by the [positive] type of binary numbers *)
 
 Require Bool.
 Require ZArith.
@@ -200,7 +200,8 @@ Proof.
   Case p; Trivial.
 Qed.
 
-Lemma ad_xor_sem_3 : (p:positive) (a':ad) (ad_bit (ad_xor (ad_x (xO p)) a') O)=(ad_bit a' O).
+Lemma ad_xor_sem_3 
+  : (p:positive) (a':ad) (ad_bit (ad_xor (ad_x (xO p)) a') O)=(ad_bit a' O).
 Proof.
   Intros. Case a'. Trivial.
   Simpl. Intro. 
@@ -219,7 +220,8 @@ Proof.
   Case (p_xor p p1); Trivial.
 Qed.
 
-Lemma ad_xor_sem_5 : (a,a':ad) (ad_bit (ad_xor a a') O)=(adf_xor (ad_bit a) (ad_bit a') O).
+Lemma ad_xor_sem_5 
+  : (a,a':ad) (ad_bit (ad_xor a a') O)=(adf_xor (ad_bit a) (ad_bit a') O).
 Proof.
   Induction a. Intro. Change (ad_bit a' O)=(xorb false (ad_bit a' O)). Rewrite false_xorb. Trivial.
   Intro. Case p. Exact ad_xor_sem_4.
@@ -258,7 +260,8 @@ Proof.
   Unfold adf_xor. Unfold 2 ad_bit. Unfold ad_bit_1. Rewrite false_xorb. Simpl.   Case p; Trivial.
 Qed.
 
-Lemma ad_xor_semantics : (a,a':ad) (eqf (ad_bit (ad_xor a a')) (adf_xor (ad_bit a) (ad_bit a'))).
+Lemma ad_xor_semantics 
+  : (a,a':ad) (eqf (ad_bit (ad_xor a a')) (adf_xor (ad_bit a) (ad_bit a'))).
 Proof.
   Unfold eqf. Intros. Generalize a a'. Elim n. Exact ad_xor_sem_5.
   Exact ad_xor_sem_6.
@@ -303,7 +306,8 @@ Proof.
   Unfold eqf. Intros. Unfold adf_xor. Rewrite H. Rewrite H0. Reflexivity.
 Qed.
 
-Lemma ad_xor_assoc : (a,a',a'':ad) (ad_xor (ad_xor a a') a'')=(ad_xor a (ad_xor a' a'')).
+Lemma ad_xor_assoc 
+  : (a,a',a'':ad) (ad_xor (ad_xor a a') a'')=(ad_xor a (ad_xor a' a'')).
 Proof.
   Intros. Apply ad_faithful.
   Apply eqf_trans with f':=(adf_xor (adf_xor (ad_bit a) (ad_bit a')) (ad_bit a'')).
@@ -354,7 +358,8 @@ Proof.
   Intros. Rewrite <- (ad_double_div_2 a0). Rewrite H. Apply ad_double_div_2.
 Qed.
 
-Lemma ad_double_plus_un_inj : (a0,a1:ad) (ad_double_plus_un a0)=(ad_double_plus_un a1) -> a0=a1.
+Lemma ad_double_plus_un_inj 
+  : (a0,a1:ad) (ad_double_plus_un a0)=(ad_double_plus_un a1) -> a0=a1.
 Proof.
   Intros. Rewrite <- (ad_double_plus_un_div_2 a0). Rewrite H. Apply ad_double_plus_un_div_2.
 Qed.
@@ -383,7 +388,8 @@ Proof.
   Intro. Discriminate H.
 Qed.
 
-Lemma ad_div_2_double_plus_un : (a:ad) (ad_bit_0 a)=true -> (ad_double_plus_un (ad_div_2 a))=a.
+Lemma ad_div_2_double_plus_un 
+  : (a:ad) (ad_bit_0 a)=true -> (ad_double_plus_un (ad_div_2 a))=a.
 Proof.
   Induction a. Intro. Discriminate H.
   Induction p. Intros. Reflexivity.
@@ -403,13 +409,15 @@ Proof.
   Induction p; Trivial.
 Qed.
 
-Lemma ad_xor_bit_0 : (a,a':ad) (ad_bit_0 (ad_xor a a'))=(xorb (ad_bit_0 a) (ad_bit_0 a')).
+Lemma ad_xor_bit_0 
+  : (a,a':ad) (ad_bit_0 (ad_xor a a'))=(xorb (ad_bit_0 a) (ad_bit_0 a')).
 Proof.
   Intros. Rewrite <- ad_bit_0_correct. Rewrite (ad_xor_semantics a a' O).
   Unfold adf_xor. Rewrite ad_bit_0_correct. Rewrite ad_bit_0_correct. Reflexivity.
 Qed.
 
-Lemma ad_xor_div_2 : (a,a':ad) (ad_div_2 (ad_xor a a'))=(ad_xor (ad_div_2 a) (ad_div_2 a')).
+Lemma ad_xor_div_2 
+  : (a,a':ad) (ad_div_2 (ad_xor a a'))=(ad_xor (ad_div_2 a) (ad_div_2 a')).
 Proof.
   Intros. Apply ad_faithful. Unfold eqf. Intro.
   Rewrite (ad_xor_semantics (ad_div_2 a) (ad_div_2 a') n).
@@ -426,7 +434,8 @@ Proof.
   Rewrite xorb_assoc. Rewrite xorb_nilpotent. Rewrite xorb_false. Reflexivity.
 Qed.
 
-Lemma ad_neg_bit_0_1 : (a,a':ad) (ad_xor a a')=(ad_x xH) -> (ad_bit_0 a)=(negb (ad_bit_0 a')).
+Lemma ad_neg_bit_0_1 
+  : (a,a':ad) (ad_xor a a')=(ad_x xH) -> (ad_bit_0 a)=(negb (ad_bit_0 a')).
 Proof.
   Intros. Apply ad_neg_bit_0. Rewrite H. Reflexivity.
 Qed.