src/HOL/Library/Fraction_Field.thy

 begin
 subclass ring_no_zero_divisors ..
 thm mult_eq_0_iff
 end
 
-instantiation fract :: (idom) "{field, division_by_zero}"
+instantiation fract :: (idom) field
 begin
 
 definition
   inverse_fract_def [code del]:
   "inverse q = Abs_fract (\<Union>x \<in> Rep_fract q.

 
 lemma divide_fract [simp]: "Fract a b / Fract c d = Fract (a * d) (b * c)"
   by (simp add: divide_fract_def)
 
 instance proof
-  show "inverse 0 = (0:: 'a fract)" by (simp add: fract_expand)
-    (simp add: fract_collapse)
-next
   fix q :: "'a fract"
   assume "q \<noteq> 0"
   then show "inverse q * q = 1" apply (cases q rule: Fract_cases_nonzero)
     by (simp_all add: mult_fract  inverse_fract fract_expand eq_fract mult_commute)
 next

   show "q / r = q * inverse r" by (simp add: divide_fract_def)
 qed
 
 end
 
-
-end
+instance fract :: (idom) division_by_zero
+proof
+  show "inverse 0 = (0:: 'a fract)" by (simp add: fract_expand)
+    (simp add: fract_collapse)
+qed
+
+
+end