changeset 4389 | 1865cb8df116 |
parent 4378 | e52f864c5b88 |
child 4423 | a129b817b58a |
--- a/src/HOL/Arith.ML Thu Dec 11 13:15:06 1997 +0100 +++ b/src/HOL/Arith.ML Fri Dec 12 10:31:25 1997 +0100 @@ -544,7 +544,7 @@ goal Arith.thy "!!k. 0<k ==> (m*k < n*k) = (m<n)"; by (safe_tac (claset() addSIs [mult_less_mono1])); by (cut_facts_tac [less_linear] 1); -by (blast_tac (claset() addDs [mult_less_mono1] addEs [less_asym]) 1); +by (blast_tac (claset() addIs [mult_less_mono1] addEs [less_asym]) 1); qed "mult_less_cancel2"; goal Arith.thy "!!k. 0<k ==> (k*m < k*n) = (m<n)";