src/HOL/Real/PNat.ML
changeset 8856 435187ffc64e
parent 7562 8519d5019309
child 8866 9ac6a18d363b
     1.1 --- a/src/HOL/Real/PNat.ML	Wed May 10 21:04:16 2000 +0200
     1.2 +++ b/src/HOL/Real/PNat.ML	Wed May 10 22:34:30 2000 +0200
     1.3 @@ -226,7 +226,8 @@
     1.4  by (auto_tac (claset() addDs [(inj_on_Abs_pnat RS inj_onD)] 
     1.5    	               addSDs [add_eq_self_zero],
     1.6  	      simpset() addsimps [sum_Rep_pnat, Rep_pnat,Abs_pnat_inverse,
     1.7 -				  Rep_pnat_gt_zero RS less_not_refl2]));
     1.8 +				  Rep_pnat_gt_zero RS less_not_refl2]
     1.9 +                        delsimprocs Nat_Numeral_Simprocs.cancel_numerals));
    1.10  qed "pnat_no_add_ident";
    1.11  
    1.12