changeset 17318 | bc1c75855f3d |
parent 17298 | ad73fb6144cf |
child 18585 | 5d379fe2eb74 |
--- 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: