src/HOL/SetInterval.thy
changeset 23277 aa158e145ea3
parent 22713 3ea6c1cb3dab
child 23398 0b5a400c7595
     1.1 --- a/src/HOL/SetInterval.thy	Wed Jun 06 17:00:09 2007 +0200
     1.2 +++ b/src/HOL/SetInterval.thy	Wed Jun 06 17:01:33 2007 +0200
     1.3 @@ -750,7 +750,7 @@
     1.4  subsection {* The formula for arithmetic sums *}
     1.5  
     1.6  lemma gauss_sum:
     1.7 -  "((1::'a::comm_semiring_1_cancel) + 1)*(\<Sum>i\<in>{1..n}. of_nat i) =
     1.8 +  "((1::'a::comm_semiring_1) + 1)*(\<Sum>i\<in>{1..n}. of_nat i) =
     1.9     of_nat n*((of_nat n)+1)"
    1.10  proof (induct n)
    1.11    case 0
    1.12 @@ -761,7 +761,7 @@
    1.13  qed
    1.14  
    1.15  theorem arith_series_general:
    1.16 -  "((1::'a::comm_semiring_1_cancel) + 1) * (\<Sum>i\<in>{..<n}. a + of_nat i * d) =
    1.17 +  "((1::'a::comm_semiring_1) + 1) * (\<Sum>i\<in>{..<n}. a + of_nat i * d) =
    1.18    of_nat n * (a + (a + of_nat(n - 1)*d))"
    1.19  proof cases
    1.20    assume ngt1: "n > 1"