--- a/src/HOL/Hyperreal/Series.ML Wed Dec 10 14:29:44 2003 +0100
+++ b/src/HOL/Hyperreal/Series.ML Wed Dec 10 15:59:34 2003 +0100
@@ -431,7 +431,7 @@
simpset() addsimps [sumr_geometric ,sums_def,
real_diff_def, real_add_divide_distrib]));
by (subgoal_tac "1 / (1 + -x) = 0/(x - 1) + - 1/(x - 1)" 1);
-by (asm_full_simp_tac (simpset() addsimps [real_divide_eq_cancel1,
+by (asm_full_simp_tac (simpset() addsimps [
real_divide_minus_eq RS sym, real_diff_def]) 2);
by (etac ssubst 1);
by (rtac LIMSEQ_add 1 THEN rtac LIMSEQ_divide 1);