# HG changeset patch
# User nipkow
# Date 902400328 -7200
# Node ID 788ccc82b1f86bf7df0b0fa4aeb340e322174f96
# Parent  70c599bff9770fae9407dd3954e87e6220ce0d20
Removed duplicate thms (see comment to Arith.ML)

diff -r 70c599bff977 -r 788ccc82b1f8 src/HOL/Real/PNat.ML
--- a/src/HOL/Real/PNat.ML	Thu Aug 06 12:45:02 1998 +0200
+++ b/src/HOL/Real/PNat.ML	Thu Aug 06 12:45:28 1998 +0200
@@ -453,16 +453,6 @@
 
 AddIffs [pnat_not_add_less1, pnat_not_add_less2];
 
-Goal "!!k::pnat. m <= n ==> m <= n + k";
-by (etac pnat_le_trans 1);
-by (rtac pnat_le_add1 1);
-qed "pnat_le_imp_add_le";
-
-Goal "!!k::pnat. m < n ==> m < n + k";
-by (etac pnat_less_le_trans 1);
-by (rtac pnat_le_add1 1);
-qed "pnat_less_imp_add_less";
-
 Goal "m + k <= n --> m <= (n::pnat)";
 by (simp_tac (simpset() addsimps [pnat_le_iff_Rep_pnat_le,
     sum_Rep_pnat_sum RS sym]) 1);