src/ZF/Constructible/WF_absolute.thy

--- 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].