# HG changeset patch
# User haftmann
# Date 1272033953 -7200
# Node ID 26eea417ccc4a87447b393e0571bc835e3bdaa54
# Parent  ed3a87a7f9773030f3be734f16e594c1f57c9468
separated instantiation of division_by_zero

diff -r ed3a87a7f977 -r 26eea417ccc4 src/HOL/Library/Fraction_Field.thy
--- 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