src/ZF/Finite.thy

--- a/src/ZF/Finite.thy	Sun Jul 14 15:11:21 2002 +0200
+++ b/src/ZF/Finite.thy	Sun Jul 14 15:14:43 2002 +0200
@@ -41,7 +41,7 @@
   type_intros Fin.intros
 
 
-subsection {* Finite powerset operator *}
+subsection {* Finite Powerset Operator *}
 
 lemma Fin_mono: "A<=B ==> Fin(A) <= Fin(B)"
 apply (unfold Fin.defs)
@@ -132,7 +132,7 @@
 done
 
 
-(*** Finite function space ***)
+subsection{*Finite Function Space*}
 
 lemma FiniteFun_mono:
     "[| A<=C;  B<=D |] ==> A -||> B  <=  C -||> D"