# HG changeset patch
# User wenzelm
# Date 1011802434 -3600
# Node ID 32c9c881dec8938114aff1c030e9b4237f7ab392
# Parent  c8ec6803d1cd3ed2db5ea968985f9b2ae67fa461
delsimps [less_Suc0];

diff -r c8ec6803d1cd -r 32c9c881dec8 src/HOL/Real/PNat.ML
--- a/src/HOL/Real/PNat.ML	Wed Jan 23 17:01:53 2002 +0100
+++ b/src/HOL/Real/PNat.ML	Wed Jan 23 17:13:54 2002 +0100
@@ -261,7 +261,7 @@
 Goalw [pnat_less_def] 
      "x < (y::pnat) ==> Rep_pnat y ~= Suc 0";
 by (auto_tac (claset(),simpset() 
-    addsimps [Rep_pnat_not_less_one] delsimps [less_one]));
+    addsimps [Rep_pnat_not_less_one] delsimps [less_Suc0]));
 qed "Rep_pnat_gt_implies_not0";
 
 Goalw [pnat_less_def]