--- a/src/Doc/manual.bib Wed Aug 02 23:15:15 2017 +0200
+++ b/src/Doc/manual.bib Thu Aug 03 08:09:15 2017 +0200
@@ -775,7 +775,7 @@
@inproceedings{Haftmann-Kraus-Kuncar-Nipkow:2013:data_refinement,
author = {Florian Haftmann and Alexander Krauss and Ond\v{r}ej Kun\v{c}ar and Tobias Nipkow},
- title = {Data Refinement in Isabelle/HOL},
+ title = {Data Refinement in {Isabelle/HOL}},
booktitle = {Interactive Theorem Proving (ITP 2013)},
pages = {100-115},
year = 2013,
@@ -1412,7 +1412,7 @@
%O
@TechReport{scala-overview-tech-report,
- author = {Martin Odersky and al.},
+ author = {Martin Odersky et al.},
title = {An Overview of the Scala Programming Language},
institution = {EPFL Lausanne, Switzerland},
year = 2004,
--- a/src/HOL/Groups_List.thy Wed Aug 02 23:15:15 2017 +0200
+++ b/src/HOL/Groups_List.thy Thu Aug 03 08:09:15 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"