--- a/src/HOL/SetInterval.thy Sun Jun 17 13:39:50 2007 +0200
+++ b/src/HOL/SetInterval.thy Sun Jun 17 18:47:03 2007 +0200
@@ -739,12 +739,11 @@
lemma geometric_sum:
"x ~= 1 ==> (\<Sum>i=0..<n. x ^ i) =
(x ^ n - 1) / (x - 1::'a::{field, recpower})"
- apply (induct "n", auto)
- apply (rule_tac c = "x - 1" in field_mult_cancel_right_lemma)
- apply (auto simp add: mult_assoc left_distrib)
- apply (simp add: times_divide_eq_right [symmetric])
- apply (simp add: right_distrib diff_minus mult_commute power_Suc)
- done
+apply (induct "n", auto)
+apply (rule_tac c = "x - 1" in field_mult_cancel_right_lemma)
+apply (auto simp add: mult_assoc left_distrib)
+apply (simp add: right_distrib diff_minus mult_commute power_Suc)
+done
subsection {* The formula for arithmetic sums *}