src/HOL/Real/PNat.ML
changeset 12842 32c9c881dec8
parent 12018 ec054019c910
equal deleted inserted replaced
12841:c8ec6803d1cd 12842:32c9c881dec8
   259 bind_thm ("Rep_pnat_less_oneE",Rep_pnat_not_less_one RS notE);
   259 bind_thm ("Rep_pnat_less_oneE",Rep_pnat_not_less_one RS notE);
   260 
   260 
   261 Goalw [pnat_less_def] 
   261 Goalw [pnat_less_def] 
   262      "x < (y::pnat) ==> Rep_pnat y ~= Suc 0";
   262      "x < (y::pnat) ==> Rep_pnat y ~= Suc 0";
   263 by (auto_tac (claset(),simpset() 
   263 by (auto_tac (claset(),simpset() 
   264     addsimps [Rep_pnat_not_less_one] delsimps [less_one]));
   264     addsimps [Rep_pnat_not_less_one] delsimps [less_Suc0]));
   265 qed "Rep_pnat_gt_implies_not0";
   265 qed "Rep_pnat_gt_implies_not0";
   266 
   266 
   267 Goalw [pnat_less_def] 
   267 Goalw [pnat_less_def] 
   268       "(x::pnat) < y | x = y | y < x";
   268       "(x::pnat) < y | x = y | y < x";
   269 by (cut_facts_tac [less_linear] 1);
   269 by (cut_facts_tac [less_linear] 1);