Various tweaks of the presentation

--- a/src/ZF/Constructible/Internalize.thy	Fri Aug 16 16:41:48 2002 +0200
+++ b/src/ZF/Constructible/Internalize.thy	Fri Aug 16 17:19:43 2002 +0200
@@ -565,6 +565,7 @@
 
 subsection{*Well-Founded Recursion!*}
 
+subsubsection{*The Operator @{term M_is_recfun}*}
 
 text{*Alternative definition, minimizing nesting of quantifiers around MH*}
 lemma M_is_recfun_iff:

--- a/src/ZF/Constructible/L_axioms.thy	Fri Aug 16 16:41:48 2002 +0200
+++ b/src/ZF/Constructible/L_axioms.thy	Fri Aug 16 17:19:43 2002 +0200
@@ -40,7 +40,7 @@
 apply (blast intro: transL)
 done
 
-subsubsection{*For L to satisfy Replacement *}
+subsection{*For L to satisfy Replacement *}
 
 (*Can't move these to Formula unless the definition of univalent is moved
 there too!*)

--- a/src/ZF/Constructible/Rec_Separation.thy	Fri Aug 16 16:41:48 2002 +0200
+++ b/src/ZF/Constructible/Rec_Separation.thy	Fri Aug 16 17:19:43 2002 +0200
@@ -172,7 +172,7 @@
 done
 
 
-subsection{*Separation for the Proof of @{text "wellfounded_on_trancl"}*}
+subsubsection{*Separation for the Proof of @{text "wellfounded_on_trancl"}*}
 
 lemma wellfounded_trancl_reflects:
   "REFLECTS[\<lambda>x. \<exists>w[L]. \<exists>wx[L]. \<exists>rp[L].

--- a/src/ZF/Constructible/WF_absolute.thy	Fri Aug 16 16:41:48 2002 +0200
+++ b/src/ZF/Constructible/WF_absolute.thy	Fri Aug 16 17:19:43 2002 +0200
@@ -601,7 +601,7 @@
 apply (simp_all add: wfrec_replacement_iff trans_eq_pair_wfrec_iff) 
 done
 
-section{*Absoluteness without assuming transitivity*}
+subsection{*Absoluteness without assuming transitivity*}
 lemma (in M_trancl) eq_pair_wfrec_iff:
   "[|wf(r);  M(r);  M(y); 
      strong_replacement(M, \<lambda>x z. \<exists>y[M]. \<exists>g[M].

--- a/src/ZF/Constructible/WFrec.thy	Fri Aug 16 16:41:48 2002 +0200
+++ b/src/ZF/Constructible/WFrec.thy	Fri Aug 16 17:19:43 2002 +0200
@@ -9,6 +9,8 @@
 theory WFrec = Wellorderings:
 
 
+subsection{*General Lemmas*}
+
 (*Many of these might be useful in WF.thy*)
 
 lemma apply_recfun2:
@@ -70,6 +72,8 @@
 apply (blast intro: sym)+
 done
 
+subsection{*Reworking of the Recursion Theory Within @{term M}*}
+
 lemma (in M_axioms) is_recfun_separation':
     "[| f \<in> r -`` {a} \<rightarrow> range(f); g \<in> r -`` {b} \<rightarrow> range(g);
         M(r); M(f); M(g); M(a); M(b) |] 
@@ -150,20 +154,6 @@
 apply (simp add: is_recfun_imp_function function_restrictI) 
 done
 
-(* ideas for further weaking the H-closure premise:
-apply (drule spec [THEN spec]) 
-apply (erule mp)
-apply (intro conjI)
-apply (blast dest!: pair_components_in_M)
-apply (blast intro!: function_restrictI dest!: pair_components_in_M)
-apply (blast intro!: function_restrictI dest!: pair_components_in_M)
-apply (simp only: subset_iff domain_iff restrict_iff vimage_iff) 
-apply (simp add: vimage_singleton_iff) 
-apply (intro allI impI conjI)
-apply (blast intro: transM dest!: pair_components_in_M)
-prefer 4;apply blast 
-*)
-
 lemma (in M_axioms) is_recfun_restrict:
      "[| wellfounded(M,r); trans(r); is_recfun(r,x,H,f); \<langle>y,x\<rangle> \<in> r; 
        M(r); M(f); 
@@ -280,6 +270,9 @@
       apply (blast dest: transM del: rev_rallE, assumption+)
 done
 
+
+subsection{*Relativization of the ZF Predicate @{term is_recfun}*}
+
 constdefs
   M_is_recfun :: "[i=>o, [i,i,i]=>o, i, i, i] => o"
    "M_is_recfun(M,MH,r,a,f) == 
@@ -339,6 +332,10 @@
 by (simp add: is_wfrec_def wfrec_replacement_def) 
 
 
+subsection{*Ordinal Arithmetic: Two Examples of Recursion*}
+
+subsubsection{*Ordinal Addition*}
+
 (*FIXME: update to use new techniques!!*)
 constdefs
  (*This expresses ordinal addition in the language of ZF.  It also 
@@ -485,7 +482,7 @@
 done
 
 
-text{*Ordinal Multiplication*}
+subsubsection{*Ordinal Multiplication*}
 
 lemma omult_eqns_unique:
      "[| omult_eqns(i,x,g,z); omult_eqns(i,x,g,z') |] ==> z=z'";