src/ZF/Constructible/Wellorderings.thy
changeset 13611 2edf034c902a
parent 13564 1500a2e48d44
child 13615 449a70d88b38
     1.1 --- a/src/ZF/Constructible/Wellorderings.thy	Mon Sep 30 16:44:00 2002 +0200
     1.2 +++ b/src/ZF/Constructible/Wellorderings.thy	Mon Sep 30 16:47:03 2002 +0200
     1.3 @@ -408,8 +408,7 @@
     1.4  
     1.5  lemma (in M_basic) omap_yields_Ord:
     1.6       "[| omap(M,A,r,f); \<langle>a,x\<rangle> \<in> f; M(a); M(x) |]  ==> Ord(x)"
     1.7 -apply (simp add: omap_def, blast) 
     1.8 -done
     1.9 +  by (simp add: omap_def)
    1.10  
    1.11  lemma (in M_basic) otype_iff:
    1.12       "[| otype(M,A,r,i); M(A); M(r); M(i) |]