src/ZF/Constructible/WF_absolute.thy
changeset 13506 acc18a5d2b1a
parent 13505 52a16cb7fefb
child 13564 1500a2e48d44
     1.1 --- a/src/ZF/Constructible/WF_absolute.thy	Fri Aug 16 16:41:48 2002 +0200
     1.2 +++ b/src/ZF/Constructible/WF_absolute.thy	Fri Aug 16 17:19:43 2002 +0200
     1.3 @@ -601,7 +601,7 @@
     1.4  apply (simp_all add: wfrec_replacement_iff trans_eq_pair_wfrec_iff) 
     1.5  done
     1.6  
     1.7 -section{*Absoluteness without assuming transitivity*}
     1.8 +subsection{*Absoluteness without assuming transitivity*}
     1.9  lemma (in M_trancl) eq_pair_wfrec_iff:
    1.10    "[|wf(r);  M(r);  M(y); 
    1.11       strong_replacement(M, \<lambda>x z. \<exists>y[M]. \<exists>g[M].