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.
Change to best_tac required to prevent looping
authorpaulson
Thu, 12 Sep 1996 10:32:43 +0200
changeset 1979 91c74763c5a3
parent 1978 e7df069acb74
child 1980 a22ff848be9b
Change to best_tac required to prevent looping
src/HOL/Arith.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/Arith.ML	Wed Sep 11 18:46:07 1996 +0200
+++ b/src/HOL/Arith.ML	Thu Sep 12 10:32:43 1996 +0200
@@ -592,7 +592,7 @@
 by (rtac disjCI 1);
 by (rtac nat_less_cases 1 THEN assume_tac 2);
 by (fast_tac (!claset addSEs [less_SucE] addss !simpset) 1);
-by (fast_tac (!claset addDs [mult_less_mono2] 
+by (best_tac (!claset addDs [mult_less_mono2] 
                       addss (!simpset addsimps [zero_less_eq RS sym])) 1);
 qed "mult_eq_self_implies_10";
isabelle