src/HOL/Hyperreal/Transcendental.thy

 lemma lemma_DERIV_ln:
      "DERIV ln z :> l ==> DERIV (%x. exp (ln x)) z :> exp (ln z) * l"
 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_hypreal)
+apply (rule_tac z = z in eq_Abs_star)
 apply (auto simp add: starfun hypreal_zero_def hypreal_less)
 done
 
 lemma hypreal_add_Infinitesimal_gt_zero:
      "[|e : Infinitesimal; 0 < x |] ==> 0 < hypreal_of_real x + e"