src/HOL/Finite_Set.thy
changeset 25303 0699e20feabd
parent 25205 b408ceba4627
child 25459 d1dce7d0731c
     1.1 --- a/src/HOL/Finite_Set.thy	Mon Nov 05 23:17:03 2007 +0100
     1.2 +++ b/src/HOL/Finite_Set.thy	Tue Nov 06 08:47:25 2007 +0100
     1.3 @@ -1199,7 +1199,7 @@
     1.4  qed
     1.5  
     1.6  lemma setsum_abs[iff]: 
     1.7 -  fixes f :: "'a => ('b::lordered_ab_group_abs)"
     1.8 +  fixes f :: "'a => ('b::pordered_ab_group_add_abs)"
     1.9    shows "abs (setsum f A) \<le> setsum (%i. abs(f i)) A"
    1.10  proof (cases "finite A")
    1.11    case True
    1.12 @@ -1215,7 +1215,7 @@
    1.13  qed
    1.14  
    1.15  lemma setsum_abs_ge_zero[iff]: 
    1.16 -  fixes f :: "'a => ('b::lordered_ab_group_abs)"
    1.17 +  fixes f :: "'a => ('b::pordered_ab_group_add_abs)"
    1.18    shows "0 \<le> setsum (%i. abs(f i)) A"
    1.19  proof (cases "finite A")
    1.20    case True
    1.21 @@ -1230,7 +1230,7 @@
    1.22  qed
    1.23  
    1.24  lemma abs_setsum_abs[simp]: 
    1.25 -  fixes f :: "'a => ('b::lordered_ab_group_abs)"
    1.26 +  fixes f :: "'a => ('b::pordered_ab_group_add_abs)"
    1.27    shows "abs (\<Sum>a\<in>A. abs(f a)) = (\<Sum>a\<in>A. abs(f a))"
    1.28  proof (cases "finite A")
    1.29    case True