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
```