src/HOL/Library/Fraction_Field.thy
changeset 36348 89c54f51f55a
parent 36331 6b9e487450ba
child 36409 d323e7773aa8
     1.1 --- a/src/HOL/Library/Fraction_Field.thy	Mon Apr 26 11:34:15 2010 +0200
     1.2 +++ b/src/HOL/Library/Fraction_Field.thy	Mon Apr 26 11:34:15 2010 +0200
     1.3 @@ -267,7 +267,7 @@
     1.4  
     1.5  end
     1.6  
     1.7 -instance fract :: (idom) division_by_zero
     1.8 +instance fract :: (idom) division_ring_inverse_zero
     1.9  proof
    1.10    show "inverse 0 = (0:: 'a fract)" by (simp add: fract_expand)
    1.11      (simp add: fract_collapse)
    1.12 @@ -450,7 +450,7 @@
    1.13          by simp
    1.14        with F have "(a * d) * (b * d) * ?F * ?F \<le> (c * b) * (b * d) * ?F * ?F"
    1.15          by (simp add: mult_le_cancel_right)
    1.16 -      with neq show ?thesis by (simp add: ring_simps)
    1.17 +      with neq show ?thesis by (simp add: field_simps)
    1.18      qed
    1.19    qed
    1.20    show "q < r ==> 0 < s ==> s * q < s * r"