src/HOL/Rat.thy
changeset 36349 39be26d1bc28
parent 36306 18c088e1c4ef
child 36409 d323e7773aa8
     1.1 --- a/src/HOL/Rat.thy	Mon Apr 26 11:34:15 2010 +0200
     1.2 +++ b/src/HOL/Rat.thy	Mon Apr 26 11:34:17 2010 +0200
     1.3 @@ -444,7 +444,7 @@
     1.4  
     1.5  end
     1.6  
     1.7 -instance rat :: division_by_zero proof
     1.8 +instance rat :: division_ring_inverse_zero proof
     1.9  qed (simp add: rat_number_expand, simp add: rat_number_collapse)
    1.10  
    1.11  
    1.12 @@ -818,7 +818,7 @@
    1.13  done
    1.14  
    1.15  lemma of_rat_inverse:
    1.16 -  "(of_rat (inverse a)::'a::{field_char_0,division_by_zero}) =
    1.17 +  "(of_rat (inverse a)::'a::{field_char_0,division_ring_inverse_zero}) =
    1.18     inverse (of_rat a)"
    1.19  by (cases "a = 0", simp_all add: nonzero_of_rat_inverse)
    1.20  
    1.21 @@ -827,7 +827,7 @@
    1.22  by (simp add: divide_inverse of_rat_mult nonzero_of_rat_inverse)
    1.23  
    1.24  lemma of_rat_divide:
    1.25 -  "(of_rat (a / b)::'a::{field_char_0,division_by_zero})
    1.26 +  "(of_rat (a / b)::'a::{field_char_0,division_ring_inverse_zero})
    1.27     = of_rat a / of_rat b"
    1.28  by (cases "b = 0") (simp_all add: nonzero_of_rat_divide)
    1.29  
    1.30 @@ -968,7 +968,7 @@
    1.31  done
    1.32  
    1.33  lemma Rats_inverse [simp]:
    1.34 -  fixes a :: "'a::{field_char_0,division_by_zero}"
    1.35 +  fixes a :: "'a::{field_char_0,division_ring_inverse_zero}"
    1.36    shows "a \<in> Rats \<Longrightarrow> inverse a \<in> Rats"
    1.37  apply (auto simp add: Rats_def)
    1.38  apply (rule range_eqI)
    1.39 @@ -984,7 +984,7 @@
    1.40  done
    1.41  
    1.42  lemma Rats_divide [simp]:
    1.43 -  fixes a b :: "'a::{field_char_0,division_by_zero}"
    1.44 +  fixes a b :: "'a::{field_char_0,division_ring_inverse_zero}"
    1.45    shows "\<lbrakk>a \<in> Rats; b \<in> Rats\<rbrakk> \<Longrightarrow> a / b \<in> Rats"
    1.46  apply (auto simp add: Rats_def)
    1.47  apply (rule range_eqI)