src/HOL/Library/Fraction_Field.thy
changeset 36312 26eea417ccc4
parent 35372 ca158c7b1144
child 36331 6b9e487450ba
     1.1 --- a/src/HOL/Library/Fraction_Field.thy	Fri Apr 23 16:38:51 2010 +0200
     1.2 +++ b/src/HOL/Library/Fraction_Field.thy	Fri Apr 23 16:45:53 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, division_by_zero}"
     1.8 +instantiation fract :: (idom) field
     1.9  begin
    1.10  
    1.11  definition
    1.12 @@ -256,9 +256,6 @@
    1.13    by (simp add: divide_fract_def)
    1.14  
    1.15  instance proof
    1.16 -  show "inverse 0 = (0:: 'a fract)" by (simp add: fract_expand)
    1.17 -    (simp add: fract_collapse)
    1.18 -next
    1.19    fix q :: "'a fract"
    1.20    assume "q \<noteq> 0"
    1.21    then show "inverse q * q = 1" apply (cases q rule: Fract_cases_nonzero)
    1.22 @@ -270,5 +267,11 @@
    1.23  
    1.24  end
    1.25  
    1.26 +instance fract :: (idom) division_by_zero
    1.27 +proof
    1.28 +  show "inverse 0 = (0:: 'a fract)" by (simp add: fract_expand)
    1.29 +    (simp add: fract_collapse)
    1.30 +qed
    1.31 +
    1.32  
    1.33  end
    1.34 \ No newline at end of file