src/HOL/Rat.thy
changeset 36306 18c088e1c4ef
parent 36112 7fa17a225852
child 36349 39be26d1bc28
     1.1 --- a/src/HOL/Rat.thy	Fri Apr 23 15:17:59 2010 +0200
     1.2 +++ b/src/HOL/Rat.thy	Fri Apr 23 15:18:00 2010 +0200
     1.3 @@ -411,7 +411,7 @@
     1.4  
     1.5  subsubsection {* The field of rational numbers *}
     1.6  
     1.7 -instantiation rat :: "{field, division_by_zero}"
     1.8 +instantiation rat :: field
     1.9  begin
    1.10  
    1.11  definition
    1.12 @@ -433,9 +433,6 @@
    1.13    by (simp add: divide_rat_def)
    1.14  
    1.15  instance proof
    1.16 -  show "inverse 0 = (0::rat)" by (simp add: rat_number_expand)
    1.17 -    (simp add: rat_number_collapse)
    1.18 -next
    1.19    fix q :: rat
    1.20    assume "q \<noteq> 0"
    1.21    then show "inverse q * q = 1" by (cases q rule: Rat_cases_nonzero)
    1.22 @@ -447,6 +444,9 @@
    1.23  
    1.24  end
    1.25  
    1.26 +instance rat :: division_by_zero proof
    1.27 +qed (simp add: rat_number_expand, simp add: rat_number_collapse)
    1.28 +
    1.29  
    1.30  subsubsection {* Various *}
    1.31