--- a/src/HOL/Hyperreal/Lim.ML Wed Dec 12 19:19:59 2001 +0100
+++ b/src/HOL/Hyperreal/Lim.ML Wed Dec 12 19:21:02 2001 +0100
@@ -1050,7 +1050,7 @@
by (asm_full_simp_tac
(simpset() addsimps [real_times_divide1_eq RS sym, NSDERIV_NSLIM_iff,
real_minus_mult_eq2, real_add_mult_distrib2 RS sym]
- delsimps [real_times_divide1_eq, real_minus_mult_eq2 RS sym]) 1);
+ delsimps [real_times_divide1_eq, real_mult_minus_eq2]) 1);
by (etac (NSLIM_const RS NSLIM_mult) 1);
qed "NSDERIV_cmult";
@@ -1063,7 +1063,7 @@
by (asm_full_simp_tac
(simpset() addsimps [real_times_divide1_eq RS sym, NSDERIV_NSLIM_iff,
real_minus_mult_eq2, real_add_mult_distrib2 RS sym]
- delsimps [real_times_divide1_eq, real_minus_mult_eq2 RS sym]) 1);
+ delsimps [real_times_divide1_eq, real_mult_minus_eq2]) 1);
by (etac (LIM_const RS LIM_mult2) 1);
qed "DERIV_cmult";
@@ -1074,7 +1074,7 @@
by (asm_full_simp_tac (simpset() addsimps [NSDERIV_NSLIM_iff]) 1);
by (res_inst_tac [("t","f x")] (real_minus_minus RS subst) 1);
by (asm_simp_tac (simpset() addsimps [real_minus_add_distrib RS sym,
- real_minus_mult_eq1 RS sym]
+ real_mult_minus_eq1]
delsimps [real_minus_add_distrib, real_minus_minus]) 1);
by (etac NSLIM_minus 1);
qed "NSDERIV_minus";
@@ -1354,8 +1354,7 @@
\ ==> DERIV (%x. inverse(f x)) x :> (- (d * inverse(f(x) ^ Suc (Suc 0))))";
by (rtac (real_mult_commute RS subst) 1);
by (asm_simp_tac (simpset() addsimps [real_minus_mult_eq1,
- realpow_inverse] delsimps [realpow_Suc,
- real_minus_mult_eq1 RS sym]) 1);
+ realpow_inverse] delsimps [realpow_Suc, real_mult_minus_eq1]) 1);
by (fold_goals_tac [o_def]);
by (blast_tac (claset() addSIs [DERIV_chain,DERIV_inverse]) 1);
qed "DERIV_inverse_fun";
@@ -1377,8 +1376,7 @@
by (asm_full_simp_tac
(simpset() addsimps [real_divide_def, real_add_mult_distrib2,
realpow_inverse,real_minus_mult_eq1] @ real_mult_ac
- delsimps [realpow_Suc, real_minus_mult_eq1 RS sym,
- real_minus_mult_eq2 RS sym]) 1);
+ delsimps [realpow_Suc, real_mult_minus_eq1, real_mult_minus_eq2]) 1);
qed "DERIV_quotient";
Goal "[| NSDERIV f x :> d; DERIV g x :> e; g(x) \\<noteq> 0 |] \
@@ -2135,8 +2133,7 @@
by (auto_tac (claset() addDs [DERIV_isCont,DERIV_unique],simpset() addsimps
[differentiable_def]));
by (auto_tac (claset() addDs [DERIV_unique],
- simpset() addsimps [real_add_mult_distrib, real_diff_def,
- real_minus_mult_eq1 RS sym]));
+ simpset() addsimps [real_add_mult_distrib, real_diff_def]));
qed "DERIV_const_ratio_const";
Goal "[|a \\<noteq> b; \\<forall>x. DERIV f x :> k |] ==> (f(b) - f(a))/(b - a) = k";
--- a/src/HOL/Hyperreal/Poly.ML Wed Dec 12 19:19:59 2001 +0100
+++ b/src/HOL/Hyperreal/Poly.ML Wed Dec 12 19:21:02 2001 +0100
@@ -361,7 +361,7 @@
by (res_inst_tac [("x","r#q")] exI 1);
by (res_inst_tac [("x","a*r + h")] exI 1);
by (case_tac "q" 1);
-by (auto_tac (claset(),simpset() addsimps [real_minus_mult_eq1 RS sym]));
+by (Auto_tac);
qed "lemma_poly_linear_rem";
Goal "EX q r. h#t = [r] +++ [-a, 1] *** q";
@@ -741,7 +741,7 @@
by Auto_tac;
by (res_inst_tac [("x","qaa +++ -- qa")] exI 1);
by (auto_tac (claset(),simpset() addsimps [poly_add,fun_eq,poly_mult,
- poly_minus,real_add_mult_distrib2,real_minus_mult_eq2 RS sym,
+ poly_minus,real_add_mult_distrib2,
ARITH_PROVE "(x = y + -z) = (z + x = (y::real))"]));
qed "poly_divides_diff";
@@ -800,8 +800,7 @@
by (induct_tac "n" 1);
by (asm_full_simp_tac (simpset() delsimps [pmult_Cons,pexp_Suc]) 1);
by (eres_inst_tac [("Pa","poly q a = 0")] swap 1);
-by (asm_full_simp_tac (simpset() addsimps [poly_add,poly_cmult,
- real_minus_mult_eq1 RS sym]) 1);
+by (asm_full_simp_tac (simpset() addsimps [poly_add,poly_cmult]) 1);
by (rtac (pexp_Suc RS ssubst) 1);
by (rtac ccontr 1);
by (asm_full_simp_tac (simpset() addsimps [poly_mult_left_cancel,
@@ -1014,8 +1013,8 @@
real_mult_ac) RS ssubst) 1);
by (rotate_tac 2 1);
by (dres_inst_tac [("x","xa")] spec 1);
-by (asm_full_simp_tac (simpset() addsimps [real_add_mult_distrib,
- real_minus_mult_eq1 RS sym] @ real_mult_ac
+by (asm_full_simp_tac (simpset()
+ addsimps [real_add_mult_distrib] @ real_mult_ac
delsimps [pmult_Cons]) 1);
qed_spec_mp "lemma_order_pderiv";
--- a/src/HOL/Hyperreal/Series.ML Wed Dec 12 19:19:59 2001 +0100
+++ b/src/HOL/Hyperreal/Series.ML Wed Dec 12 19:21:02 2001 +0100
@@ -86,7 +86,7 @@
Goal "sumr 0 n f + -(real n * r) = sumr 0 n (%i. f i + -r)";
by (full_simp_tac (simpset() addsimps [sumr_add RS sym,
- real_minus_mult_eq2] delsimps [real_minus_mult_eq2 RS sym]) 1);
+ real_minus_mult_eq2] delsimps [real_mult_minus_eq2]) 1);
qed "sumr_add_mult_const";
Goalw [real_diff_def]
--- a/src/HOL/Hyperreal/Transcendental.ML Wed Dec 12 19:19:59 2001 +0100
+++ b/src/HOL/Hyperreal/Transcendental.ML Wed Dec 12 19:21:02 2001 +0100
@@ -2089,7 +2089,6 @@
by (auto_tac (claset() addSIs [sin_gt_zero2,cos_gt_zero_pi]
addSIs [real_mult_order,
real_inverse_gt_0],simpset()));
-by (rtac (CLAIM "-x < y ==> -y < (x::real)") 1 THEN Auto_tac);
qed "tan_gt_zero";
Goal "[| - pi/2 < x; x < 0 |] ==> tan x < 0";
@@ -2170,7 +2169,6 @@
by (Step_tac 1);
by (res_inst_tac [("x","-x")] exI 2);
by (auto_tac (claset() addSIs [exI],simpset()));
-by (rtac (CLAIM "-x < y ==> -y < (x::real)") 1 THEN Auto_tac);
qed "lemma_tan_total1";
Goal "EX! x. -(pi/2) < x & x < (pi/2) & tan x = y";
--- a/src/HOL/Real/HahnBanach/Aux.thy Wed Dec 12 19:19:59 2001 +0100
+++ b/src/HOL/Real/HahnBanach/Aux.thy Wed Dec 12 19:21:02 2001 +0100
@@ -74,7 +74,7 @@
hence "x * (- z) \<le> y * (- z)"
by (rule real_mult_le_le_mono2)
hence "- (x * z) \<le> - (y * z)"
- by (simp only: real_minus_mult_eq2)
+ by (simp only: real_mult_minus_eq2)
thus ?thesis by (simp only: real_mult_commute)
qed