src/HOL/Arith.ML
changeset 5758 27a2b36efd95
parent 5654 8b872d546b9e
child 5771 7c2c8cf20221
     1.1 --- a/src/HOL/Arith.ML	Fri Oct 23 20:36:21 1998 +0200
     1.2 +++ b/src/HOL/Arith.ML	Fri Oct 23 20:44:34 1998 +0200
     1.3 @@ -212,10 +212,10 @@
     1.4  
     1.5  (*needs !!k for add_ac to work*)
     1.6  Goal "!!k:: nat. [| k<l;  m+l = k+n |] ==> m<n";
     1.7 -by (auto_tac (claset(),
     1.8 +by (force_tac (claset(),
     1.9  	      simpset() delsimps [add_Suc_right]
    1.10  	                addsimps [less_iff_Suc_add,
    1.11 -				  add_Suc_right RS sym] @ add_ac));
    1.12 +				  add_Suc_right RS sym] @ add_ac) 1);
    1.13  qed "less_add_eq_less";
    1.14  
    1.15