src/ZF/Finite.thy

     consI:   "[| a: A;  b: B;  h: A -||> B;  a ~: domain(h) |]
               ==> cons(<a,b>,h) : A -||> B"
   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)
 apply (rule lfp_mono)
 apply (rule Fin.bnd_mono)+

 apply (simp add: succ_def mem_not_refl [THEN cons_fun_eq])
 apply (fast intro!: Fin.consI)
 done
 
 
-(*** Finite function space ***)
+subsection{*Finite Function Space*}
 
 lemma FiniteFun_mono:
     "[| A<=C;  B<=D |] ==> A -||> B  <=  C -||> D"
 apply (unfold FiniteFun.defs)
 apply (rule lfp_mono)