From 352a92bcee8bc4e338a2493ad8e7cb0299c68563 Mon Sep 17 00:00:00 2001
From: desmettr
Date: Wed, 31 Jul 2002 09:48:04 +0000
Subject: MAJ pour Exp_prop

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

diff --git a/theories/Reals/Ranalysis4.v b/theories/Reals/Ranalysis4.v
index b2287efc26..52cfb2a7af 100644
--- a/theories/Reals/Ranalysis4.v
+++ b/theories/Reals/Ranalysis4.v
@@ -19,6 +19,7 @@ Require Ranalysis1.
 Require R_sqrt.
 Require Ranalysis2.
 Require Ranalysis3.
+Require Export Exp_prop.
 Require Export Rtrigo_reg.
 Require Export Sqrt_reg.
 
@@ -237,8 +238,6 @@ Intros; Unfold derivable; Intro; Apply derivable_pt_finite_sum.
 Qed.
 
 (* Regularity of hyperbolic functions *)
-Axiom derivable_pt_lim_exp : (x:R) (derivable_pt_lim exp x (exp x)).   
-
 Lemma derivable_pt_lim_cosh : (x:R) (derivable_pt_lim cosh x ``(sinh x)``).
 Intro.
 Unfold cosh sinh; Unfold Rdiv.
-- 
cgit v1.2.3