# HG changeset patch
# User huffman
# Date 1180997643 -7200
# Node ID 5f12b40a95bfb93a2f824122311b38799333ebab
# Parent  7077dc80a14bc10502eef0b9546fa86f37e20d90
add lemma exp_of_real

diff -r 7077dc80a14b -r 5f12b40a95bf src/HOL/Hyperreal/Transcendental.thy
--- a/src/HOL/Hyperreal/Transcendental.thy	Mon Jun 04 22:27:18 2007 +0200
+++ b/src/HOL/Hyperreal/Transcendental.thy	Tue Jun 05 00:54:03 2007 +0200
@@ -726,6 +726,13 @@
 unfolding exp_def
 by (simp only: Cauchy_product summable_norm_exp exp_series_add)
 
+lemma exp_of_real: "exp (of_real x) = of_real (exp x)"
+unfolding exp_def
+apply (subst of_real.suminf)
+apply (rule summable_exp_generic)
+apply (simp add: scaleR_conv_of_real)
+done
+
 lemma exp_ge_add_one_self_aux: "0 \<le> (x::real) ==> (1 + x) \<le> exp(x)"
 apply (drule order_le_imp_less_or_eq, auto)
 apply (simp add: exp_def)