src/HOL/Equiv_Relations.thy
changeset 40945 b8703f63bfb2
parent 40817 781da1e8808c
child 44204 3cdc4176638c
     1.1 --- a/src/HOL/Equiv_Relations.thy	Fri Dec 03 20:26:57 2010 +0100
     1.2 +++ b/src/HOL/Equiv_Relations.thy	Fri Dec 03 20:38:58 2010 +0100
     1.3 @@ -315,7 +315,7 @@
     1.4  
     1.5  subsection {* Quotients and finiteness *}
     1.6  
     1.7 -text {*Suggested by Florian Kammüller*}
     1.8 +text {*Suggested by Florian Kammüller*}
     1.9  
    1.10  lemma finite_quotient: "finite A ==> r \<subseteq> A \<times> A ==> finite (A//r)"
    1.11    -- {* recall @{thm equiv_type} *}