# HG changeset patch
# User haftmann
# Date 1272028680 -7200
# Node ID 18c088e1c4efcd7f94b04c92d86a2f0236ac570b
# Parent  dbe99291eb3ca2def086faba13176ff0c3b99250
separated instantiation of division_by_zero

diff -r dbe99291eb3c -r 18c088e1c4ef src/HOL/Rat.thy
--- a/src/HOL/Rat.thy	Fri Apr 23 15:17:59 2010 +0200
+++ b/src/HOL/Rat.thy	Fri Apr 23 15:18:00 2010 +0200
@@ -411,7 +411,7 @@
 
 subsubsection {* The field of rational numbers *}
 
-instantiation rat :: "{field, division_by_zero}"
+instantiation rat :: field
 begin
 
 definition
@@ -433,9 +433,6 @@
   by (simp add: divide_rat_def)
 
 instance proof
-  show "inverse 0 = (0::rat)" by (simp add: rat_number_expand)
-    (simp add: rat_number_collapse)
-next
   fix q :: rat
   assume "q \<noteq> 0"
   then show "inverse q * q = 1" by (cases q rule: Rat_cases_nonzero)
@@ -447,6 +444,9 @@
 
 end
 
+instance rat :: division_by_zero proof
+qed (simp add: rat_number_expand, simp add: rat_number_collapse)
+
 
 subsubsection {* Various *}