src/ZF/Constructible/L_axioms.thy
changeset 13268 240509babf00
parent 13223 45be08fbdcff
child 13269 3ba9be497c33
     1.1 --- a/src/ZF/Constructible/L_axioms.thy	Mon Jul 01 18:10:53 2002 +0200
     1.2 +++ b/src/ZF/Constructible/L_axioms.thy	Mon Jul 01 18:16:18 2002 +0200
     1.3 @@ -62,8 +62,7 @@
     1.4  
     1.5  lemma replacement: "replacement(L,P)"
     1.6  apply (simp add: replacement_def, clarify)
     1.7 -apply (frule LReplace_in_L, assumption+)
     1.8 -apply clarify 
     1.9 +apply (frule LReplace_in_L, assumption+, clarify) 
    1.10  apply (rule_tac x=Y in exI)   
    1.11  apply (simp add: Replace_iff univalent_def, blast) 
    1.12  done