Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Faster proof of mult_less_cancel2
authorpaulson
Fri, 12 Dec 1997 10:31:25 +0100
changeset 4389 1865cb8df116
parent 4388 c54f2e3423f2
child 4390 57e16404c2a9
Faster proof of mult_less_cancel2
src/HOL/Arith.ML file | annotate | diff | comparison | revisions 
--- 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)";
isabelle