src/HOL/Nonstandard_Analysis/HDeriv.thy

   apply (subgoal_tac "( *f* of_real) \<epsilon> \<in> Infinitesimal - {0::'a star}")
    apply (simp only: nsderiv_def)
    apply (drule (1) bspec)+
    apply (drule (1) approx_trans3)
    apply simp
-  apply (simp add: Infinitesimal_of_hypreal Infinitesimal_epsilon)
+  apply (simp add: Infinitesimal_of_hypreal)
   apply (simp add: of_hypreal_eq_0_iff hypreal_epsilon_not_zero)
   done
 
 text \<open>First \<open>NSDERIV\<close> in terms of \<open>NSLIM\<close>.\<close>
 

   by (simp add: NSDERIV_NSLIM_iff DERIV_LIM_iff LIM_NSLIM_iff [symmetric])
 
 text \<open>While we're at it!\<close>
 lemma NSDERIV_iff2:
   "(NSDERIV f x :> D) \<longleftrightarrow>
-    (\<forall>w. w \<noteq> star_of x & w \<approx> star_of x \<longrightarrow> ( *f* (%z. (f z - f x) / (z-x))) w \<approx> star_of D)"
+    (\<forall>w. w \<noteq> star_of x \<and> w \<approx> star_of x \<longrightarrow> ( *f* (\<lambda>z. (f z - f x) / (z - x))) w \<approx> star_of D)"
   by (simp add: NSDERIV_NSLIM_iff2 NSLIM_def)
 
 (* FIXME delete *)
 lemma hypreal_not_eq_minus_iff: "x \<noteq> a \<longleftrightarrow> x - a \<noteq> (0::'a::ab_group_add)"
   by auto

   apply (auto simp add: NSDERIV_iff2)
   apply (case_tac "u = hypreal_of_real x", auto)
   apply (drule_tac x = u in spec, auto)
   apply (drule_tac c = "u - hypreal_of_real x" and b = "hypreal_of_real D" in approx_mult1)
    apply (drule_tac [!] hypreal_not_eq_minus_iff [THEN iffD1])
-   apply (subgoal_tac [2] "( *f* (%z. z-x)) u \<noteq> (0::hypreal) ")
+   apply (subgoal_tac [2] "( *f* (\<lambda>z. z - x)) u \<noteq> (0::hypreal) ")
     apply (auto simp: approx_minus_iff [THEN iffD1, THEN mem_infmal_iff [THEN iffD2]]
       Infinitesimal_subset_HFinite [THEN subsetD])
   done
 
 lemma NSDERIVD4:

   apply (frule_tac f = g in NSDERIV_approx)
     apply (auto simp add: starfun_lambda_cancel2 starfun_o [symmetric])
   apply (case_tac "( *f* g) (star_of (x) + xa) = star_of (g x) ")
    apply (drule_tac g = g in NSDERIV_zero)
       apply (auto simp add: divide_inverse)
-  apply (rule_tac z1 = "( *f* g) (star_of (x) + xa) - star_of (g x) " and y1 = "inverse xa" in lemma_chain [THEN ssubst])
+  apply (rule_tac z1 = "( *f* g) (star_of (x) + xa) - star_of (g x) " and y1 = "inverse xa"
+      in lemma_chain [THEN ssubst])
    apply (erule hypreal_not_eq_minus_iff [THEN iffD1])
   apply (rule approx_mult_star_of)
    apply (simp_all add: divide_inverse [symmetric])
    apply (blast intro: NSDERIVD1 approx_minus_iff [THEN iffD2])
   apply (blast intro: NSDERIVD2)