src/HOL/Hyperreal/Transcendental.thy

--- a/src/HOL/Hyperreal/Transcendental.thy	Fri Sep 09 17:47:37 2005 +0200
+++ b/src/HOL/Hyperreal/Transcendental.thy	Fri Sep 09 19:34:22 2005 +0200
@@ -2473,8 +2473,8 @@
 by (erule DERIV_fun_exp)
 
 lemma STAR_exp_ln: "0 < z ==> ( *f* (%x. exp (ln x))) z = z"
-apply (rule_tac z = z in eq_Abs_star)
-apply (auto simp add: starfun hypreal_zero_def hypreal_less)
+apply (cases z)
+apply (auto simp add: starfun star_n_zero_num star_n_less star_n_eq_iff)
 done
 
 lemma hypreal_add_Infinitesimal_gt_zero: