# HG changeset patch
# User nipkow
# Date 1501690922 -7200
# Node ID b6a0d95b94be9a60b93f50fbaea9278853eb0cdc
# Parent  7454317f883cd73f15cd2a47bc6c81458e35ea8a
generalized lemma

diff -r 7454317f883c -r b6a0d95b94be src/HOL/Groups_List.thy
--- a/src/HOL/Groups_List.thy	Tue Aug 01 22:19:37 2017 +0200
+++ b/src/HOL/Groups_List.thy	Wed Aug 02 18:22:02 2017 +0200
@@ -142,9 +142,9 @@
   "m \<le> n \<Longrightarrow> sum_list [m..<n] = \<Sum> {m..<n}"
 by(simp add: distinct_sum_list_conv_Sum)
 
-lemma sum_list_eq_0_nat_iff_nat [simp]:
-  "sum_list ns = (0::nat) \<longleftrightarrow> (\<forall>n \<in> set ns. n = 0)"
-  by (induct ns) simp_all
+lemma (in canonically_ordered_monoid_add) sum_list_eq_0_iff [simp]:
+  "sum_list ns = 0 \<longleftrightarrow> (\<forall>n \<in> set ns. n = 0)"
+by (induct ns) simp_all
 
 lemma member_le_sum_list_nat:
   "(n :: nat) \<in> set ns \<Longrightarrow> n \<le> sum_list ns"