src/ZF/Constructible/WF_absolute.thy
changeset 13615 449a70d88b38
parent 13564 1500a2e48d44
child 13634 99a593b49b04
     1.1 --- a/src/ZF/Constructible/WF_absolute.thy	Tue Oct 01 11:17:25 2002 +0200
     1.2 +++ b/src/ZF/Constructible/WF_absolute.thy	Tue Oct 01 13:26:10 2002 +0200
     1.3 @@ -225,7 +225,6 @@
     1.4  
     1.5  lemma (in M_trancl) wellfounded_trancl:
     1.6       "[|wellfounded(M,r); M(r)|] ==> wellfounded(M,r^+)"
     1.7 -apply (rotate_tac -1)
     1.8  apply (simp add: wellfounded_iff_wellfounded_on_field)
     1.9  apply (rule wellfounded_on_subset_A, erule wellfounded_on_trancl)
    1.10     apply blast