src/HOL/Hyperreal/SEQ.thy
changeset 18585 5d379fe2eb74
parent 17439 a358da1a0218
child 19765 dfe940911617
     1.1 --- a/src/HOL/Hyperreal/SEQ.thy	Thu Jan 05 22:29:53 2006 +0100
     1.2 +++ b/src/HOL/Hyperreal/SEQ.thy	Thu Jan 05 22:29:55 2006 +0100
     1.3 @@ -436,7 +436,7 @@
     1.4  apply (auto intro!: lessI [THEN less_imp_le] dest!: less_imp_Suc_add)
     1.5  apply (induct_tac "ka")
     1.6  apply (auto intro: order_trans)
     1.7 -apply (erule swap) 
     1.8 +apply (erule contrapos_np)
     1.9  apply (induct_tac "k")
    1.10  apply (auto intro: order_trans)
    1.11  done