# HG changeset patch
# User nipkow
# Date 1501738285 -7200
# Node ID ca985e87c123fbbe8fe4ec53df08b052657fd609
# Parent  50ed697e97f17fc10c200b08da87528ea6d3d86f# Parent  b6a0d95b94be9a60b93f50fbaea9278853eb0cdc
merged

diff -r 50ed697e97f1 -r ca985e87c123 src/HOL/Groups_List.thy
--- a/src/HOL/Groups_List.thy	Tue Aug 01 20:38:39 2017 +0200
+++ b/src/HOL/Groups_List.thy	Thu Aug 03 07:31:25 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"