| changeset 4195 | 7f7bf0bd0f63 |
| parent 4089 | 96fba19bcbe2 |
| child 4746 | a5dcd7e4a37d |
--- a/src/HOL/Integ/Equiv.ML Mon Nov 10 15:06:58 1997 +0100 +++ b/src/HOL/Integ/Equiv.ML Mon Nov 10 15:25:12 1997 +0100 @@ -241,7 +241,7 @@ qed "congruent2_commuteI"; -(*** Cardinality results suggested by Florian Kammüller ***) +(*** Cardinality results suggested by Florian Kammueller ***) (*Recall that equiv A r implies r <= A Times A (equiv_type) *) goal thy "!!A. [| finite A; r <= A Times A |] ==> finite (A/r)";