src/ZF/Constructible/Wellorderings.thy
changeset 13780 af7b79271364
parent 13634 99a593b49b04
child 16417 9bc16273c2d4
     1.1 --- a/src/ZF/Constructible/Wellorderings.thy	Wed Jan 15 16:44:21 2003 +0100
     1.2 +++ b/src/ZF/Constructible/Wellorderings.thy	Wed Jan 15 16:45:32 2003 +0100
     1.3 @@ -84,7 +84,7 @@
     1.4  lemma  (in M_basic) wellfounded_on_iff_wellfounded:
     1.5       "wellfounded_on(M,A,r) <-> wellfounded(M, r \<inter> A*A)"
     1.6  apply (simp add: wellfounded_on_def wellfounded_def, safe)
     1.7 - apply blast 
     1.8 + apply force
     1.9  apply (drule_tac x=x in rspec, assumption, blast) 
    1.10  done
    1.11