src/HOL/SetInterval.thy
changeset 31017 2c227493ea56
parent 30384 2f24531b2d3e
child 31044 6896c2498ac0
     1.1 --- a/src/HOL/SetInterval.thy	Tue Apr 28 15:50:30 2009 +0200
     1.2 +++ b/src/HOL/SetInterval.thy	Tue Apr 28 15:50:30 2009 +0200
     1.3 @@ -855,7 +855,7 @@
     1.4  
     1.5  lemma geometric_sum:
     1.6    "x ~= 1 ==> (\<Sum>i=0..<n. x ^ i) =
     1.7 -  (x ^ n - 1) / (x - 1::'a::{field, recpower})"
     1.8 +  (x ^ n - 1) / (x - 1::'a::{field})"
     1.9  by (induct "n") (simp_all add:field_simps power_Suc)
    1.10  
    1.11  subsection {* The formula for arithmetic sums *}