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