--- a/src/HOL/Library/Fraction_Field.thy Fri Apr 23 16:38:51 2010 +0200
+++ b/src/HOL/Library/Fraction_Field.thy Fri Apr 23 16:45:53 2010 +0200
@@ -232,7 +232,7 @@
thm mult_eq_0_iff
end
-instantiation fract :: (idom) "{field, division_by_zero}"
+instantiation fract :: (idom) field
begin
definition
@@ -256,9 +256,6 @@
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)
@@ -270,5 +267,11 @@
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
\ No newline at end of file