# HG changeset patch
# User paulson
# Date 842517163 -7200
# Node ID 91c74763c5a373a557039bb3b0b235de13144ff3
# Parent  e7df069acb741c5f4ace028681cc4feb6531cb75
Change to best_tac required to prevent looping

diff -r e7df069acb74 -r 91c74763c5a3 src/HOL/Arith.ML
--- 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";