src/HOL/Hyperreal/Lim.ML

 by (cut_inst_tac
     [("P","%(u,v). a \\<le> u & u \\<le> v & v \\<le> b --> ~(f(u) \\<le> y & y \\<le> f(v))")] 
     lemma_BOLZANO2 1);
 by Safe_tac;
 by (ALLGOALS(Asm_full_simp_tac));
-by (Blast_tac 2);
 by (asm_full_simp_tac (simpset() addsimps [isCont_iff,LIM_def]) 1);
 by (rtac ccontr 1);
 by (subgoal_tac "a \\<le> x & x \\<le> b" 1);
 by (Asm_full_simp_tac 2);
 by (dres_inst_tac [("P", "%d. 0<d --> ?P d"),("x","1")] spec 2);

 by (dres_inst_tac [("x","-h")] spec 1);
 by (asm_full_simp_tac
     (simpset() addsimps [real_abs_def, real_inverse_eq_divide, 
                          pos_real_less_divide_eq,
                          symmetric real_diff_def]
-               addsplits [split_if_asm]) 1);
+               addsplits [split_if_asm]
+               delsimprocs [fast_real_arith_simproc]) 1);
 by (subgoal_tac "0 < (f (x - h) - f x)/h" 1);
 by (arith_tac 2);
 by (asm_full_simp_tac
     (simpset() addsimps [pos_real_less_divide_eq]) 1); 
 qed "DERIV_left_dec";

 by (res_inst_tac [("x1","a"),("y1","xa")] (order_le_imp_less_or_eq RS disjE) 5);
 by (assume_tac 5);
 by (dres_inst_tac [("z","xa"),("w","b")] real_le_anti_sym 5);
 by (REPEAT(Asm_full_simp_tac 2));
 by (dtac real_dense 1 THEN etac exE 1);
-by (res_inst_tac [("x","r")] exI 1 THEN Asm_full_simp_tac 1);
+by (res_inst_tac [("x","r")] exI 1 THEN Asm_simp_tac 1);
 by (etac conjE 1);
 by (forw_inst_tac [("a","a"),("x","r")] lemma_interval 1);
 by (EVERY1[assume_tac, etac exE]);
 by (subgoal_tac "(\\<exists>l. DERIV f r :> l) & \
 \        (\\<exists>d. 0 < d & (\\<forall>y. abs(r - y) < d --> f(r) = f(y)))" 1);

 
 (* Gallileo's "trick": average velocity = av. of end velocities *)
 Goal "[|a \\<noteq> (b::real); \\<forall>x. DERIV v x :> k|] \
 \     ==> v((a + b)/2) = (v a + v b)/2";
 by (res_inst_tac [("R1.0","a"),("R2.0","b")] real_linear_less2 1);
-by Auto_tac;
+by Safe_tac;
 by (ftac DERIV_const_ratio_const2 1 THEN assume_tac 1);
 by (ftac DERIV_const_ratio_const2 2 THEN assume_tac 2);
 by (dtac real_less_half_sum 1);
 by (dtac real_gt_half_sum 2); 
 by (ftac (real_not_refl2 RS DERIV_const_ratio_const2) 1 THEN assume_tac 1);