Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
delsimps [less_Suc0];
authorwenzelm
Wed, 23 Jan 2002 17:13:54 +0100
changeset 12842 32c9c881dec8
parent 12841 c8ec6803d1cd
child 12843 50bd380e6675
delsimps [less_Suc0];
src/HOL/Real/PNat.ML file | annotate | diff | comparison | revisions 
--- 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]
isabelle