Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
eliminated non-ASCII;
authorwenzelm
Fri, 06 Jun 1997 21:49:47 +0200
changeset 3430 d21b920363ab
parent 3429 160f18a686b5
child 3431 05b397185e1d
eliminated non-ASCII;
src/HOL/Finite.ML file | annotate | diff | comparison | revisions 
--- 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) -->  \
isabelle