--- a/src/ZF/Cardinal_AC.thy Sun Jul 14 15:11:21 2002 +0200
+++ b/src/ZF/Cardinal_AC.thy Sun Jul 14 15:14:43 2002 +0200
@@ -10,7 +10,7 @@
theory Cardinal_AC = CardinalArith + Zorn:
-(*** Strengthened versions of existing theorems about cardinals ***)
+subsection{*Strengthened Forms of Existing Theorems on Cardinals*}
lemma cardinal_eqpoll: "|A| eqpoll A"
apply (rule AC_well_ord [THEN exE])
@@ -65,7 +65,7 @@
done
-(*** Other applications of AC ***)
+subsection{*Other Applications of AC*}
lemma Card_le_imp_lepoll: "|A| le |B| ==> A lepoll B"
apply (rule cardinal_eqpoll