--- 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 *}