src/HOL/Arith.ML

--- a/src/HOL/Arith.ML	Thu Aug 06 12:44:07 1998 +0200
+++ b/src/HOL/Arith.ML	Thu Aug 06 12:45:02 1998 +0200
@@ -179,16 +179,6 @@
 qed "not_add_less2";
 AddIffs [not_add_less1, not_add_less2];
 
-Goal "!!k::nat. m <= n ==> m <= n+k";
-by (etac le_trans 1);
-by (rtac le_add1 1);
-qed "le_imp_add_le";
-
-Goal "!!k::nat. m < n ==> m < n+k";
-by (etac less_le_trans 1);
-by (rtac le_add1 1);
-qed "less_imp_add_less";
-
 Goal "m+k<=n --> m<=(n::nat)";
 by (induct_tac "k" 1);
 by (ALLGOALS Asm_simp_tac);