src/ZF/List.thy
changeset 13611 2edf034c902a
parent 13524 604d0f3622d6
child 13615 449a70d88b38
     1.1 --- a/src/ZF/List.thy	Mon Sep 30 16:44:00 2002 +0200
     1.2 +++ b/src/ZF/List.thy	Mon Sep 30 16:47:03 2002 +0200
     1.3 @@ -1089,7 +1089,6 @@
     1.4  apply (simp add: nth_append le_iff split add: nat_diff_split)
     1.5  apply (auto dest!: not_lt_imp_le 
     1.6              simp add: nth_append diff_self_eq_0 less_diff_conv add_commute)
     1.7 -apply (drule_tac j = x in lt_trans2, auto)
     1.8  done
     1.9  
    1.10  lemma take_upt [rule_format,simp]: