changeset 14398 | c5c47703f763 |
parent 14387 | e96d5c42c4b0 |
child 14421 | ee97b6463cb4 |
--- a/src/HOL/Integ/IntDef.thy Thu Feb 19 10:41:32 2004 +0100 +++ b/src/HOL/Integ/IntDef.thy Thu Feb 19 15:57:34 2004 +0100 @@ -521,7 +521,6 @@ apply (simp add: order_le_less) apply (case_tac "w < 0") apply (simp add: order_less_imp_le) - apply (blast intro: order_less_trans) apply (simp add: linorder_not_less) done