src/ZF/Ordinal.thy
changeset 14864 419b45cdb400
parent 14565 c6dc17aab88a
child 16417 9bc16273c2d4
--- a/src/ZF/Ordinal.thy	Tue Jun 01 18:52:38 2004 +0200
+++ b/src/ZF/Ordinal.thy	Wed Jun 02 17:35:08 2004 +0200
@@ -293,7 +293,7 @@
 by (unfold Memrel_def, blast)
 
 lemma relation_Memrel: "relation(Memrel(A))"
-by (simp add: relation_def Memrel_def, blast)
+by (simp add: relation_def Memrel_def)
 
 (*The membership relation (as a set) is well-founded.
   Proof idea: show A<=B by applying the foundation axiom to A-B *)