src/ZF/Constructible/WF_absolute.thy
changeset 13418 7c0ba9dba978
parent 13382 b37764a46b16
child 13428 99e52e78eb65
     1.1 --- a/src/ZF/Constructible/WF_absolute.thy	Wed Jul 24 16:16:44 2002 +0200
     1.2 +++ b/src/ZF/Constructible/WF_absolute.thy	Wed Jul 24 17:59:12 2002 +0200
     1.3 @@ -568,7 +568,7 @@
     1.4  apply (drule_tac x1=x and x="\<lambda>x\<in>r -`` {x}. wfrec(r, x, H)" 
     1.5         in rspec [THEN rspec]) 
     1.6  apply (simp_all add: function_lam) 
     1.7 -apply (blast intro: dest: pair_components_in_M ) 
     1.8 +apply (blast intro: lam_closed dest: pair_components_in_M ) 
     1.9  done
    1.10  
    1.11  text{*Eliminates one instance of replacement.*}