src/HOL/Hyperreal/MacLaurin.ML

 by DERIV_tac;
 by (rtac lemma_DERIV_subst 3);
 by (rtac DERIV_quotient 3);
 by (rtac DERIV_const 4);
 by (rtac DERIV_pow 3);
-by (asm_simp_tac (simpset() addsimps [real_inverse_distrib,
+by (asm_simp_tac (simpset() addsimps [inverse_mult_distrib,
     CLAIM_SIMP "(a::real) * b * c * (d * e) = a * b * (c * d) * e" 
-    real_mult_ac,fact_diff_Suc]) 4);
+    mult_ac,fact_diff_Suc]) 4);
 by (Asm_simp_tac 3);
 by (forw_inst_tac [("m","ma")] less_add_one 2);
 by (Clarify_tac 2);
 by (asm_simp_tac (simpset() addsimps 
     [CLAIM "Suc m = ma + d + 1 ==> m - ma = d"]

 by (rtac DERIV_cmult 2);
 by (rtac lemma_DERIV_subst 2);
 by DERIV_tac;
 by (stac fact_Suc 2);
 by (stac real_of_nat_mult 2);
-by (simp_tac (simpset() addsimps [real_inverse_distrib] @
-    real_mult_ac) 2);
+by (simp_tac (simpset() addsimps [inverse_mult_distrib] @
+    mult_ac) 2);
 by (subgoal_tac "ALL ma. ma < n --> \
 \        (EX t. 0 < t & t < h & difg (Suc ma) t = 0)" 1);
 by (rotate_tac 11 1);
 by (dres_inst_tac [("x","m")] spec 1);
 by (etac impE 1);

 by (cut_inst_tac [("f","%x. f (-x)"),
                  ("diff","%n x. ((- 1) ^ n) * diff n (-x)"),
                  ("h","-h"),("n","n")] Maclaurin_objl 1);
 by (Asm_full_simp_tac 1);
 by (etac impE 1 THEN Step_tac 1);
-by (stac real_minus_mult_eq2 1);
+by (stac minus_mult_right 1);
 by (rtac DERIV_cmult 1);
 by (rtac lemma_DERIV_subst 1);
 by (rtac (read_instantiate [("g","uminus")] DERIV_chain2) 1);
 by (rtac DERIV_minus 2 THEN rtac DERIV_Id 2);
 by (Force_tac 2);

 Goal "d < (4::nat) ==> d = 0 | d = 1 | d = 2 | d = 3";
 by (case_tac "d" 1 THEN Auto_tac);
 qed "lemma_exhaust_less_4";
 
 bind_thm ("real_mult_le_lemma",
-          simplify (simpset()) (inst "y" "1" real_mult_le_le_mono2));
+          simplify (simpset()) (inst "b" "1" mult_right_mono));
 
 
 Goal "abs(sin x - \
 \          sumr 0 n (%m. (if even m then 0 \
 \                         else ((- 1) ^ ((m - (Suc 0)) div 2)) / real (fact m)) * \

 by (asm_simp_tac (simpset() addsimps [even_num_iff]) 2);
 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,real_mult_le_le_mono2],
+by (auto_tac (claset() addSIs [real_mult_le_lemma,mult_right_mono],
       simpset() addsimps [real_divide_def,abs_mult,abs_inverse,realpow_abs RS
 sym]));
 qed "Maclaurin_sin_bound";
 
 Goal "0 < n --> Suc (Suc (2 * n - 2)) = 2*n";

 by (arith_tac 1);
 by (rtac (CLAIM "[|x = y; x' = y'|] ==> x + x' = y + (y'::real)") 1);
 by (rtac sumr_fun_eq 1);
 by (auto_tac (claset(),simpset() addsimps [odd_not_even RS sym]));
 by (auto_tac (claset(),simpset() addsimps [odd_Suc_mult_two_ex,
-    even_mult_two_ex,real_add_mult_distrib,cos_add]  delsimps 
+    even_mult_two_ex,left_distrib,cos_add]  delsimps 
     [fact_Suc,realpow_Suc]));
 by (auto_tac (claset(),simpset() addsimps [real_mult_commute]));
 qed "Maclaurin_cos_expansion";
 
 Goal "[| 0 < x; 0 < n |] ==> \

 by (assume_tac 1 THEN assume_tac 1);
 by (rtac (CLAIM "[|x = y; x' = y'|] ==> x + x' = y + (y'::real)") 1);
 by (rtac sumr_fun_eq 1);
 by (auto_tac (claset(),simpset() addsimps [odd_not_even RS sym]));
 by (auto_tac (claset(),simpset() addsimps [odd_Suc_mult_two_ex,
-    even_mult_two_ex,real_add_mult_distrib,cos_add]  delsimps 
+    even_mult_two_ex,left_distrib,cos_add]  delsimps 
     [fact_Suc,realpow_Suc]));
 by (auto_tac (claset(),simpset() addsimps [real_mult_commute]));
 qed "Maclaurin_cos_expansion2";
 
 Goal "[| x < 0; 0 < n |] ==> \

 by (assume_tac 1 THEN assume_tac 1);
 by (rtac (CLAIM "[|x = y; x' = y'|] ==> x + x' = y + (y'::real)") 1);
 by (rtac sumr_fun_eq 1);
 by (auto_tac (claset(),simpset() addsimps [odd_not_even RS sym]));
 by (auto_tac (claset(),simpset() addsimps [odd_Suc_mult_two_ex,
-    even_mult_two_ex,real_add_mult_distrib,cos_add]  delsimps 
+    even_mult_two_ex,left_distrib,cos_add]  delsimps 
     [fact_Suc,realpow_Suc]));
 by (auto_tac (claset(),simpset() addsimps [real_mult_commute]));
 qed "Maclaurin_minus_cos_expansion";
 
 (* ------------------------------------------------------------------------- *)