src/HOL/Library/Nat_Infinity.thy

   by default (simp add: of_nat_eq_Fin)
 
 
 subsection {* Ordering *}
 
-instantiation inat :: ordered_ab_semigroup_add
+instantiation inat :: linordered_ab_semigroup_add
 begin
 
 definition
   [code del]: "m \<le> n = (case n of Fin n1 \<Rightarrow> (case m of Fin m1 \<Rightarrow> m1 \<le> n1 | \<infinity> \<Rightarrow> False)
     | \<infinity> \<Rightarrow> True)"

 instance by default
   (auto simp add: less_eq_inat_def less_inat_def plus_inat_def split: inat.splits)
 
 end
 
-instance inat :: pordered_comm_semiring
+instance inat :: ordered_comm_semiring
 proof
   fix a b c :: inat
   assume "a \<le> b" and "0 \<le> c"
   thus "c * a \<le> c * b"
     unfolding times_inat_def less_eq_inat_def zero_inat_def