src/ZF/Integ/Int.ML
changeset 5758 27a2b36efd95
parent 5561 426c1e330903
child 6153 bff90585cce5
     1.1 --- a/src/ZF/Integ/Int.ML	Fri Oct 23 20:36:21 1998 +0200
     1.2 +++ b/src/ZF/Integ/Int.ML	Fri Oct 23 20:44:34 1998 +0200
     1.3 @@ -172,7 +172,7 @@
     1.4  qed "zmagnitude_int_of";
     1.5  
     1.6  Goalw [zmagnitude_def] "n: nat ==> zmagnitude($~ $# n) = n";
     1.7 -by (auto_tac(claset() addDs [not_znegative_imp_zero], simpset()));
     1.8 +by (force_tac(claset() addDs [not_znegative_imp_zero], simpset())1);
     1.9  qed "zmagnitude_zminus_int_of";
    1.10  
    1.11  Addsimps [zmagnitude_int_of, zmagnitude_zminus_int_of];