1.1 --- a/src/HOL/Real/PReal.thy	Tue May 11 14:00:02 2004 +0200
     1.2 +++ b/src/HOL/Real/PReal.thy	Tue May 11 20:11:08 2004 +0200
     1.3 @@ -15,7 +15,7 @@
     1.4  
     1.5  text{*As a special case, the sum of two positives is positive.  One of the
     1.6  premises could be weakened to the relation @{text "\<le>"}.*}
     1.7 -lemma pos_add_strict: "[|0<a; b<c|] ==> b < a + (c::'a::ordered_semiring)"
     1.8 +lemma pos_add_strict: "[|0<a; b<c|] ==> b < a + (c::'a::ordered_semidom)"
     1.9  by (insert add_strict_mono [of 0 a b c], simp)
    1.10  
    1.11  lemma interval_empty_iff: