# HG changeset patch
# User nipkow
# Date 902400302 -7200
# Node ID 70c599bff9770fae9407dd3954e87e6220ce0d20
# Parent  3155ccd9a5069956f9bd41a06f17671bf471dc99
Removed duplicate thms:
less_imp_add_less = trans_less_add1
le_imp_add_le = trans_le_add1

diff -r 3155ccd9a506 -r 70c599bff977 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);