src/ZF/Constructible/Wellorderings.thy
changeset 13245 714f7a423a15
parent 13223 45be08fbdcff
child 13247 e3c289f0724b
--- a/src/ZF/Constructible/Wellorderings.thy	Mon Jun 24 11:59:14 2002 +0200
+++ b/src/ZF/Constructible/Wellorderings.thy	Mon Jun 24 11:59:21 2002 +0200
@@ -144,10 +144,10 @@
 apply (blast dest: transM) 
 done
 
-lemma (in M_axioms) pred_closed [intro]: 
+lemma (in M_axioms) pred_closed [intro,simp]: 
      "[| M(A); M(r); M(x) |] ==> M(Order.pred(A,x,r))"
 apply (simp add: Order.pred_def) 
-apply (insert pred_separation [of r x], simp, blast) 
+apply (insert pred_separation [of r x], simp) 
 done
 
 lemma (in M_axioms) membership_abs [simp]: 
@@ -170,10 +170,10 @@
 apply (blast dest: transM)
 done 
 
-lemma (in M_axioms) Memrel_closed [intro]: 
+lemma (in M_axioms) Memrel_closed [intro,simp]: 
      "M(A) ==> M(Memrel(A))"
 apply (simp add: M_Memrel_iff) 
-apply (insert Memrel_separation, simp, blast)
+apply (insert Memrel_separation, simp)
 done