src/ZF/OrdQuant.thy
changeset 13244 7b37e218f298
parent 13175 81082cfa5618
child 13253 edbf32029d33
     1.1 --- a/src/ZF/OrdQuant.thy	Mon Jun 24 11:58:21 2002 +0200
     1.2 +++ b/src/ZF/OrdQuant.thy	Mon Jun 24 11:59:14 2002 +0200
     1.3 @@ -58,11 +58,7 @@
     1.4  apply (blast intro: lt_Ord2) 
     1.5  done
     1.6  
     1.7 -(** Now some very basic ZF theorems **)
     1.8 -
     1.9 -(*FIXME: move to Rel.thy*)
    1.10 -lemma trans_imp_trans_on: "trans(r) ==> trans[A](r)"
    1.11 -by (unfold trans_def trans_on_def, blast)
    1.12 +(** Union over ordinals **)
    1.13  
    1.14  lemma Ord_OUN [intro,simp]:
    1.15       "[| !!x. x<A ==> Ord(B(x)) |] ==> Ord(\<Union>x<A. B(x))"