--- a/src/ZF/Epsilon.thy Sun Jul 14 15:11:21 2002 +0200
+++ b/src/ZF/Epsilon.thy Sun Jul 14 15:14:43 2002 +0200
@@ -34,7 +34,7 @@
"rec(k,a,b) == recursor(a,b,k)"
-(*** Basic closure properties ***)
+subsection{*Basic Closure Properties*}
lemma arg_subset_eclose: "A <= eclose(A)"
apply (unfold eclose_def)
@@ -77,7 +77,7 @@
by (rule arg_in_eclose_sing [THEN eclose_induct], blast)
-(*** Leastness of eclose ***)
+subsection{*Leastness of @{term eclose}*}
(** eclose(A) is the least transitive set including A as a subset. **)
@@ -117,7 +117,7 @@
done
-(*** Epsilon recursion ***)
+subsection{*Epsilon Recursion*}
(*Unused...*)
lemma mem_eclose_trans: "[| A: eclose(B); B: eclose(C) |] ==> A: eclose(C)"
@@ -205,7 +205,7 @@
dest: Ord_in_Ord [THEN eclose_sing_Ord, THEN subsetD])
done
-(*** Rank ***)
+subsection{*Rank*}
(*NOT SUITABLE FOR REWRITING -- RECURSIVE!*)
lemma rank: "rank(a) = (UN y:a. succ(rank(y)))"
@@ -309,7 +309,7 @@
done
-(*** Corollaries of leastness ***)
+subsection{*Corollaries of Leastness*}
lemma mem_eclose_subset: "A:B ==> eclose(A)<=eclose(B)"
apply (rule Transset_eclose [THEN eclose_least])