# HG changeset patch
# User wenzelm
# Date 865626587 -7200
# Node ID d21b920363abfb038d504c1a0367715d64a51efc
# Parent  160f18a686b5befd8001b701d3998f6c775cde1e
eliminated non-ASCII;

diff -r 160f18a686b5 -r d21b920363ab src/HOL/Finite.ML
--- a/src/HOL/Finite.ML	Fri Jun 06 19:30:06 1997 +0200
+++ b/src/HOL/Finite.ML	Fri Jun 06 21:49:47 1997 +0200
@@ -430,7 +430,7 @@
 qed_spec_mp "psubset_card" ;
 
 
-(*Relates to equivalence classes.   Based on a theorem of F. Kammüller's.
+(*Relates to equivalence classes.   Based on a theorem of F. Kammueller's.
   The "finite C" premise is redundant*)
 goal thy "!!C. finite C ==> finite (Union C) --> \
 \          (! c : C. k dvd card c) -->  \