src/HOL/Arith.ML
changeset 5270 70c599bff977
parent 5183 89f162de39cf
child 5316 7a8975451a89
     1.1 --- a/src/HOL/Arith.ML	Thu Aug 06 12:44:07 1998 +0200
     1.2 +++ b/src/HOL/Arith.ML	Thu Aug 06 12:45:02 1998 +0200
     1.3 @@ -179,16 +179,6 @@
     1.4  qed "not_add_less2";
     1.5  AddIffs [not_add_less1, not_add_less2];
     1.6  
     1.7 -Goal "!!k::nat. m <= n ==> m <= n+k";
     1.8 -by (etac le_trans 1);
     1.9 -by (rtac le_add1 1);
    1.10 -qed "le_imp_add_le";
    1.11 -
    1.12 -Goal "!!k::nat. m < n ==> m < n+k";
    1.13 -by (etac less_le_trans 1);
    1.14 -by (rtac le_add1 1);
    1.15 -qed "less_imp_add_less";
    1.16 -
    1.17  Goal "m+k<=n --> m<=(n::nat)";
    1.18  by (induct_tac "k" 1);
    1.19  by (ALLGOALS Asm_simp_tac);