From c0ecd40e650b9e8c5b0b0f86c2a6aafde07f41be Mon Sep 17 00:00:00 2001
From: desmettr
Date: Wed, 22 Jan 2003 14:10:09 +0000
Subject: Commentaires

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3581 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 theories/Reals/Rpower.v | 7 +++----
 1 file changed, 3 insertions(+), 4 deletions(-)

diff --git a/theories/Reals/Rpower.v b/theories/Reals/Rpower.v
index 0f213e05e9..5ac341355c 100644
--- a/theories/Reals/Rpower.v
+++ b/theories/Reals/Rpower.v
@@ -10,8 +10,7 @@
 (*i Due to L.Thery i*) 
 
 (************************************************************)
-(* Preuve de l'existence de log et de la fonction puissance *)
-(* Propriétés                                               *)
+(* Definitions of log and Rpower : R->R->R; main properties *)
 (************************************************************)
 
 Require Rbase.
@@ -152,10 +151,10 @@ Assert H3 := (exp_pos x); Red; Intro; Rewrite H4 in H3; Elim (Rlt_antirefl ? H3)
 Apply Rinv_neq_R0; Red; Intro; Rewrite H3 in H; Elim (Rlt_antirefl ? H).
 Qed.
 
-(* Définition du log népérien R+*>R *)
+(* Definition of log R+* -> R *)
 Definition Rln [y:posreal] : R := Cases (ln_exists (pos y) (RIneq.cond_pos y)) of (existTT a b) => a end.
 
-(* Une extension sur R *)
+(* Extension on R *)
 Definition ln : R->R := [x:R](Cases (total_order_Rlt R0 x) of
       (leftT a) => (Rln (mkposreal x a)) 
     | (rightT a) => R0 end).
-- 
cgit v1.2.3