diff -r 77ea79aed99d -r 83f1a514dcb4 src/HOL/Hyperreal/HyperNat.thy
--- a/src/HOL/Hyperreal/HyperNat.thy	Tue May 11 14:00:02 2004 +0200
+++ b/src/HOL/Hyperreal/HyperNat.thy	Tue May 11 20:11:08 2004 +0200
@@ -158,7 +158,7 @@
 apply (simp add: hypnat_zero_def hypnat_add)
 done
 
-instance hypnat :: plus_ac0
+instance hypnat :: comm_monoid_add
   by intro_classes
     (assumption |
       rule hypnat_add_commute hypnat_add_assoc hypnat_add_zero_left)+
@@ -280,13 +280,10 @@
 declare hypnat_zero_not_eq_one [THEN not_sym, simp]
 
 
-text{*The Hypernaturals Form A Semiring*}
-instance hypnat :: semiring
+text{*The Hypernaturals Form A comm_semiring_1_cancel*}
+instance hypnat :: comm_semiring_1_cancel
 proof
   fix i j k :: hypnat
-  show "(i + j) + k = i + (j + k)" by (rule hypnat_add_assoc)
-  show "i + j = j + i" by (rule hypnat_add_commute)
-  show "0 + i = i" by simp
   show "(i * j) * k = i * (j * k)" by (rule hypnat_mult_assoc)
   show "i * j = j * i" by (rule hypnat_mult_commute)
   show "1 * i = i" by (rule hypnat_mult_1)
@@ -352,9 +349,9 @@
 done
 
 
-subsection{*The Hypernaturals Form an Ordered Semiring*}
+subsection{*The Hypernaturals Form an Ordered comm_semiring_1_cancel*}
 
-instance hypnat :: ordered_semiring
+instance hypnat :: ordered_semidom
 proof
   fix x y z :: hypnat
   show "0 < (1::hypnat)"
@@ -456,7 +453,7 @@
 qed
 
 
-subsection{*The Embedding @{term hypnat_of_nat} Preserves Ring and 
+subsection{*The Embedding @{term hypnat_of_nat} Preserves comm_ring_1 and 
       Order Properties*}
 
 constdefs