Mercurial Mercurial > wneuper > isa / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | bz2 | gz | help
delsimps [less_Suc0];
authorwenzelm
Wed, 23 Jan 2002 17:13:54 +0100
changeset 1284232c9c881dec8
parent 12841 c8ec6803d1cd
child 12843 50bd380e6675
delsimps [less_Suc0];
src/HOL/Real/PNat.ML file | annotate | diff | comparison | revisions 
     1.1 --- a/src/HOL/Real/PNat.ML	Wed Jan 23 17:01:53 2002 +0100
     1.2 +++ b/src/HOL/Real/PNat.ML	Wed Jan 23 17:13:54 2002 +0100
     1.3 @@ -261,7 +261,7 @@
     1.4  Goalw [pnat_less_def] 
     1.5       "x < (y::pnat) ==> Rep_pnat y ~= Suc 0";
     1.6  by (auto_tac (claset(),simpset() 
     1.7 -    addsimps [Rep_pnat_not_less_one] delsimps [less_one]));
     1.8 +    addsimps [Rep_pnat_not_less_one] delsimps [less_Suc0]));
     1.9  qed "Rep_pnat_gt_implies_not0";
    1.10  
    1.11  Goalw [pnat_less_def]
wneuper/isa