1.1 --- a/src/HOL/Algebra/abstract/Ring.thy	Tue May 11 14:00:02 2004 +0200
     1.2 +++ b/src/HOL/Algebra/abstract/Ring.thy	Tue May 11 20:11:08 2004 +0200
     1.3 @@ -117,37 +117,37 @@
     1.4  
     1.5  (* Basic facts --- move to HOL!!! *)
     1.6  
     1.7 -lemma natsum_0 [simp]: "setsum f {..(0::nat)} = (f 0::'a::plus_ac0)"
     1.8 +lemma natsum_0 [simp]: "setsum f {..(0::nat)} = (f 0::'a::comm_monoid_add)"
     1.9  by simp
    1.10  
    1.11  lemma natsum_Suc [simp]:
    1.12 -  "setsum f {..Suc n} = (f (Suc n) + setsum f {..n}::'a::plus_ac0)"
    1.13 +  "setsum f {..Suc n} = (f (Suc n) + setsum f {..n}::'a::comm_monoid_add)"
    1.14  by (simp add: atMost_Suc)
    1.15  
    1.16  lemma natsum_Suc2:
    1.17 -  "setsum f {..Suc n} = (setsum (%i. f (Suc i)) {..n} + f 0::'a::plus_ac0)"
    1.18 +  "setsum f {..Suc n} = (setsum (%i. f (Suc i)) {..n} + f 0::'a::comm_monoid_add)"
    1.19  proof (induct n)
    1.20    case 0 show ?case by simp
    1.21  next
    1.22 -  case Suc thus ?case by (simp add: plus_ac0.assoc) 
    1.23 +  case Suc thus ?case by (simp add: semigroup_add.add_assoc) 
    1.24  qed
    1.25  
    1.26  lemma natsum_cong [cong]:
    1.27 -  "!!k. [| j = k; !!i::nat. i <= k ==> f i = (g i::'a::plus_ac0) |] ==>
    1.28 +  "!!k. [| j = k; !!i::nat. i <= k ==> f i = (g i::'a::comm_monoid_add) |] ==>
    1.29          setsum f {..j} = setsum g {..k}"
    1.30  by (induct j) auto
    1.31  
    1.32 -lemma natsum_zero [simp]: "setsum (%i. 0) {..n::nat} = (0::'a::plus_ac0)"
    1.33 +lemma natsum_zero [simp]: "setsum (%i. 0) {..n::nat} = (0::'a::comm_monoid_add)"
    1.34  by (induct n) simp_all
    1.35  
    1.36  lemma natsum_add [simp]:
    1.37 -  "!!f::nat=>'a::plus_ac0.
    1.38 +  "!!f::nat=>'a::comm_monoid_add.
    1.39     setsum (%i. f i + g i) {..n::nat} = setsum f {..n} + setsum g {..n}"
    1.40 -by (induct n) (simp_all add: plus_ac0)
    1.41 +by (induct n) (simp_all add: add_ac)
    1.42  
    1.43  (* Facts specific to rings *)
    1.44  
    1.45 -instance ring < plus_ac0
    1.46 +instance ring < comm_monoid_add
    1.47  proof
    1.48    fix x y z
    1.49    show "(x::'a::ring) + y = y + x" by (rule a_comm)