src/ZF/Constructible/WF_absolute.thy
changeset 13363 c26eeb000470
parent 13353 1800e7134d2e
child 13382 b37764a46b16
     1.1 --- a/src/ZF/Constructible/WF_absolute.thy	Tue Jul 16 16:28:49 2002 +0200
     1.2 +++ b/src/ZF/Constructible/WF_absolute.thy	Tue Jul 16 16:29:36 2002 +0200
     1.3 @@ -611,19 +611,6 @@
     1.4  apply (simp add: wfrec_relativize, blast) 
     1.5  done
     1.6  
     1.7 -lemma (in M_wfrank) wfrec_closed_lemma [rule_format]:
     1.8 -     "[|wf(r); M(r); 
     1.9 -        strong_replacement(M, \<lambda>x y. y = \<langle>x, wfrec(r, x, H)\<rangle>);
    1.10 -        \<forall>x[M]. \<forall>g[M]. function(g) --> M(H(x,g)) |] 
    1.11 -      ==> M(a) --> M(wfrec(r,a,H))"
    1.12 -apply (rule_tac a=a in wf_induct, assumption+)
    1.13 -apply (subst wfrec, assumption, clarify)
    1.14 -apply (drule_tac x1=x and x="\<lambda>x\<in>r -`` {x}. wfrec(r, x, H)" 
    1.15 -       in rspec [THEN rspec]) 
    1.16 -apply (simp_all add: function_lam) 
    1.17 -apply (blast intro: dest: pair_components_in_M ) 
    1.18 -done
    1.19 -
    1.20  text{*Full version not assuming transitivity, but maybe not very useful.*}
    1.21  theorem (in M_wfrank) wfrec_closed:
    1.22       "[|wf(r); M(r); M(a);