diff -r fa22ae64ed85 -r b8703f63bfb2 src/HOL/Finite_Set.thy --- a/src/HOL/Finite_Set.thy Fri Dec 03 20:26:57 2010 +0100 +++ b/src/HOL/Finite_Set.thy Fri Dec 03 20:38:58 2010 +0100 @@ -2277,7 +2277,7 @@ apply (blast elim!: equalityE) done -text {* Relates to equivalence classes. Based on a theorem of F. Kammüller. *} +text {* Relates to equivalence classes. Based on a theorem of F. Kammüller. *} lemma dvd_partition: "finite (Union C) ==>