src/HOL/Arith.ML
changeset 4356 0dfd34f0d33d
parent 4297 5defc2105cc8
child 4360 40e5c97e988d
     1.1 --- a/src/HOL/Arith.ML	Wed Dec 03 12:55:04 1997 +0100
     1.2 +++ b/src/HOL/Arith.ML	Wed Dec 03 17:25:43 1997 +0100
     1.3 @@ -536,6 +536,7 @@
     1.4  by (induct_tac "n" 2);
     1.5  by (ALLGOALS Asm_simp_tac);
     1.6  qed "zero_less_mult_iff";
     1.7 +Addsimps [zero_less_mult_iff];
     1.8  
     1.9  goal Arith.thy "(m*n = 1) = (m=1 & n=1)";
    1.10  by (induct_tac "m" 1);
    1.11 @@ -544,6 +545,7 @@
    1.12  by (Simp_tac 1);
    1.13  by (fast_tac (claset() addss simpset()) 1);
    1.14  qed "mult_eq_1_iff";
    1.15 +Addsimps [mult_eq_1_iff];
    1.16  
    1.17  goal Arith.thy "!!k. 0<k ==> (m*k < n*k) = (m<n)";
    1.18  by (safe_tac (claset() addSIs [mult_less_mono1]));
    1.19 @@ -594,8 +596,7 @@
    1.20  by (rtac disjCI 1);
    1.21  by (rtac nat_less_cases 1 THEN assume_tac 2);
    1.22  by (fast_tac (claset() addSEs [less_SucE] addss simpset()) 1);
    1.23 -by (best_tac (claset() addDs [mult_less_mono2] 
    1.24 -                      addss (simpset() addsimps [zero_less_eq RS sym])) 1);
    1.25 +by (best_tac (claset() addDs [mult_less_mono2] addss simpset()) 1);
    1.26  qed "mult_eq_self_implies_10";
    1.27  
    1.28