src/HOL/Library/Fraction_Field.thy
changeset 36409 d323e7773aa8
parent 36348 89c54f51f55a
child 36414 a19ba9bbc8dc
     1.1 --- a/src/HOL/Library/Fraction_Field.thy	Mon Apr 26 11:34:19 2010 +0200
     1.2 +++ b/src/HOL/Library/Fraction_Field.thy	Mon Apr 26 15:37:50 2010 +0200
     1.3 @@ -232,7 +232,7 @@
     1.4  thm mult_eq_0_iff
     1.5  end
     1.6  
     1.7 -instantiation fract :: (idom) field
     1.8 +instantiation fract :: (idom) field_inverse_zero
     1.9  begin
    1.10  
    1.11  definition
    1.12 @@ -263,16 +263,13 @@
    1.13  next
    1.14    fix q r :: "'a fract"
    1.15    show "q / r = q * inverse r" by (simp add: divide_fract_def)
    1.16 +next
    1.17 +  show "inverse 0 = (0:: 'a fract)" by (simp add: fract_expand)
    1.18 +    (simp add: fract_collapse)
    1.19  qed
    1.20  
    1.21  end
    1.22  
    1.23 -instance fract :: (idom) division_ring_inverse_zero
    1.24 -proof
    1.25 -  show "inverse 0 = (0:: 'a fract)" by (simp add: fract_expand)
    1.26 -    (simp add: fract_collapse)
    1.27 -qed
    1.28 -
    1.29  
    1.30  subsubsection {* The ordered field of fractions over an ordered idom *}
    1.31