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