src/ZF/Finite.thy
changeset 13356 c9cfe1638bf2
parent 13328 703de709a64b
child 13524 604d0f3622d6
     1.1 --- a/src/ZF/Finite.thy	Sun Jul 14 15:11:21 2002 +0200
     1.2 +++ b/src/ZF/Finite.thy	Sun Jul 14 15:14:43 2002 +0200
     1.3 @@ -41,7 +41,7 @@
     1.4    type_intros Fin.intros
     1.5  
     1.6  
     1.7 -subsection {* Finite powerset operator *}
     1.8 +subsection {* Finite Powerset Operator *}
     1.9  
    1.10  lemma Fin_mono: "A<=B ==> Fin(A) <= Fin(B)"
    1.11  apply (unfold Fin.defs)
    1.12 @@ -132,7 +132,7 @@
    1.13  done
    1.14  
    1.15  
    1.16 -(*** Finite function space ***)
    1.17 +subsection{*Finite Function Space*}
    1.18  
    1.19  lemma FiniteFun_mono:
    1.20      "[| A<=C;  B<=D |] ==> A -||> B  <=  C -||> D"