1.1 --- a/src/HOL/Hyperreal/HyperNat.thy	Tue May 11 14:00:02 2004 +0200
     1.2 +++ b/src/HOL/Hyperreal/HyperNat.thy	Tue May 11 20:11:08 2004 +0200
     1.3 @@ -158,7 +158,7 @@
     1.4  apply (simp add: hypnat_zero_def hypnat_add)
     1.5  done
     1.6  
     1.7 -instance hypnat :: plus_ac0
     1.8 +instance hypnat :: comm_monoid_add
     1.9    by intro_classes
    1.10      (assumption |
    1.11        rule hypnat_add_commute hypnat_add_assoc hypnat_add_zero_left)+
    1.12 @@ -280,13 +280,10 @@
    1.13  declare hypnat_zero_not_eq_one [THEN not_sym, simp]
    1.14  
    1.15  
    1.16 -text{*The Hypernaturals Form A Semiring*}
    1.17 -instance hypnat :: semiring
    1.18 +text{*The Hypernaturals Form A comm_semiring_1_cancel*}
    1.19 +instance hypnat :: comm_semiring_1_cancel
    1.20  proof
    1.21    fix i j k :: hypnat
    1.22 -  show "(i + j) + k = i + (j + k)" by (rule hypnat_add_assoc)
    1.23 -  show "i + j = j + i" by (rule hypnat_add_commute)
    1.24 -  show "0 + i = i" by simp
    1.25    show "(i * j) * k = i * (j * k)" by (rule hypnat_mult_assoc)
    1.26    show "i * j = j * i" by (rule hypnat_mult_commute)
    1.27    show "1 * i = i" by (rule hypnat_mult_1)
    1.28 @@ -352,9 +349,9 @@
    1.29  done
    1.30  
    1.31  
    1.32 -subsection{*The Hypernaturals Form an Ordered Semiring*}
    1.33 +subsection{*The Hypernaturals Form an Ordered comm_semiring_1_cancel*}
    1.34  
    1.35 -instance hypnat :: ordered_semiring
    1.36 +instance hypnat :: ordered_semidom
    1.37  proof
    1.38    fix x y z :: hypnat
    1.39    show "0 < (1::hypnat)"
    1.40 @@ -456,7 +453,7 @@
    1.41  qed
    1.42  
    1.43  
    1.44 -subsection{*The Embedding @{term hypnat_of_nat} Preserves Ring and 
    1.45 +subsection{*The Embedding @{term hypnat_of_nat} Preserves comm_ring_1 and 
    1.46        Order Properties*}
    1.47  
    1.48  constdefs