# HG changeset patch
# User paulson
# Date 881919085 -3600
# Node ID 1865cb8df1165e4d6af5a32485f57aaa796921d8
# Parent  c54f2e3423f2c568697a30f08d371a565c7f314f
Faster proof of mult_less_cancel2

diff -r c54f2e3423f2 -r 1865cb8df116 src/HOL/Arith.ML
--- 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)";