| changeset 40945 | b8703f63bfb2 |
| parent 40922 | 4d0f96a54e76 |
| child 41550 | efa734d9b221 |
--- 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) ==>