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