src/ZF/Constructible/Wellorderings.thy
changeset 13245 714f7a423a15
parent 13223 45be08fbdcff
child 13247 e3c289f0724b
     1.1 --- a/src/ZF/Constructible/Wellorderings.thy	Mon Jun 24 11:59:14 2002 +0200
     1.2 +++ b/src/ZF/Constructible/Wellorderings.thy	Mon Jun 24 11:59:21 2002 +0200
     1.3 @@ -144,10 +144,10 @@
     1.4  apply (blast dest: transM) 
     1.5  done
     1.6  
     1.7 -lemma (in M_axioms) pred_closed [intro]: 
     1.8 +lemma (in M_axioms) pred_closed [intro,simp]: 
     1.9       "[| M(A); M(r); M(x) |] ==> M(Order.pred(A,x,r))"
    1.10  apply (simp add: Order.pred_def) 
    1.11 -apply (insert pred_separation [of r x], simp, blast) 
    1.12 +apply (insert pred_separation [of r x], simp) 
    1.13  done
    1.14  
    1.15  lemma (in M_axioms) membership_abs [simp]: 
    1.16 @@ -170,10 +170,10 @@
    1.17  apply (blast dest: transM)
    1.18  done 
    1.19  
    1.20 -lemma (in M_axioms) Memrel_closed [intro]: 
    1.21 +lemma (in M_axioms) Memrel_closed [intro,simp]: 
    1.22       "M(A) ==> M(Memrel(A))"
    1.23  apply (simp add: M_Memrel_iff) 
    1.24 -apply (insert Memrel_separation, simp, blast)
    1.25 +apply (insert Memrel_separation, simp)
    1.26  done
    1.27  
    1.28