src/HOL/Library/Fraction_Field.thy
changeset 36414 a19ba9bbc8dc
parent 36409 d323e7773aa8
child 37765 26bdfb7b680b
     1.1 --- a/src/HOL/Library/Fraction_Field.thy	Tue Apr 27 08:18:25 2010 +0200
     1.2 +++ b/src/HOL/Library/Fraction_Field.thy	Tue Apr 27 09:49:36 2010 +0200
     1.3 @@ -431,7 +431,7 @@
     1.4  
     1.5  end
     1.6  
     1.7 -instance fract :: (linordered_idom) linordered_field
     1.8 +instance fract :: (linordered_idom) linordered_field_inverse_zero
     1.9  proof
    1.10    fix q r s :: "'a fract"
    1.11    show "q \<le> r ==> s + q \<le> s + r"