src/HOL/Hyperreal/MacLaurin.ML

 by (asm_simp_tac (HOL_ss addsimps 
     [CLAIM "(a::real) * (b * (c * d)) = (d * a) * (b * c)"]
      delsimps [realpow_Suc]) 2);
 by (stac real_mult_inv_left 2);
 by (stac real_mult_inv_left 3);
-by (dtac (realpow_gt_zero RS real_not_refl2 RS not_sym) 2);
-by (assume_tac 2);
+by (rtac (real_not_refl2 RS not_sym) 2);
+by (etac zero_less_power 2);
 by (rtac real_of_nat_fact_not_zero 2);
 by (Simp_tac 2);
 by (etac exE 1);
 by (cut_inst_tac [("b","%t. f t - \
 \      (sumr 0 n (%m. (diff m 0 / real (fact m)) * (t ^ m)) + \

 by (rtac (CLAIM "[| x = x'; y = y' |] ==> x + y = x' + (y'::real)") 1);
 by (rtac sumr_fun_eq 1);
 by (Asm_full_simp_tac 1);
 by (auto_tac (claset(),simpset() addsimps [real_divide_def,
     CLAIM "((a * b) * c) * d = (b * c) * (a * (d::real))",
-    realpow_mult RS sym]));
+    power_mult_distrib RS sym]));
 qed "Maclaurin_minus";
 
 Goal "(h < 0 & 0 < n & diff 0 = f & \
 \      (ALL m t. \
 \         m < n & h <= t & t <= 0 --> DERIV (diff m) t :> diff (Suc m) t))\

 by (dtac lemma_even_mod_4_div_2 1);
 by (asm_full_simp_tac (simpset() addsimps [numeral_2_eq_2,real_divide_def]) 1);
 by (dtac lemma_odd_mod_4_div_2 1);
 by (asm_full_simp_tac (simpset() addsimps [numeral_2_eq_2, real_divide_def]) 1);
 by (auto_tac (claset() addSIs [real_mult_le_lemma,mult_right_mono],
-      simpset() addsimps [real_divide_def,abs_mult,abs_inverse,realpow_abs RS
+      simpset() addsimps [real_divide_def,abs_mult,abs_inverse,power_abs RS
 sym]));
 qed "Maclaurin_sin_bound";
 
 Goal "0 < n --> Suc (Suc (2 * n - 2)) = 2*n";
 by (induct_tac "n" 1);

 \                      x ^ m)) \
 \     + ((sin(t + 1/2 * real (n) *pi) / real (fact n)) * x ^ n)";
 by (cut_inst_tac [("f","sin"),("n","n"),("x","x"),
        ("diff","%n x. sin(x + 1/2*real (n)*pi)")] 
        Maclaurin_all_lt_objl 1);
-by (Step_tac 1);
+by (Safe_tac);
 by (Simp_tac 1);
 by (Simp_tac 1);
 by (case_tac "n" 1);
 by (Clarify_tac 1); 
 by (Asm_full_simp_tac 1);