src/HOL/Groebner_Basis.thy
changeset 36349 39be26d1bc28
parent 36305 dbe99291eb3c
child 36409 d323e7773aa8
     1.1 --- a/src/HOL/Groebner_Basis.thy	Mon Apr 26 11:34:15 2010 +0200
     1.2 +++ b/src/HOL/Groebner_Basis.thy	Mon Apr 26 11:34:17 2010 +0200
     1.3 @@ -474,20 +474,20 @@
     1.4    fieldgb "op +" "op *" "op ^" "0::'a::{field,number_ring}" "1" "op -" "uminus" "op /" "inverse" apply (unfold_locales) by (simp_all add: divide_inverse)
     1.5  
     1.6  lemma divide_Numeral1: "(x::'a::{field,number_ring}) / Numeral1 = x" by simp
     1.7 -lemma divide_Numeral0: "(x::'a::{field,number_ring, division_by_zero}) / Numeral0 = 0"
     1.8 +lemma divide_Numeral0: "(x::'a::{field,number_ring, division_ring_inverse_zero}) / Numeral0 = 0"
     1.9    by simp
    1.10 -lemma mult_frac_frac: "((x::'a::{field,division_by_zero}) / y) * (z / w) = (x*z) / (y*w)"
    1.11 +lemma mult_frac_frac: "((x::'a::{field,division_ring_inverse_zero}) / y) * (z / w) = (x*z) / (y*w)"
    1.12    by simp
    1.13 -lemma mult_frac_num: "((x::'a::{field, division_by_zero}) / y) * z  = (x*z) / y"
    1.14 +lemma mult_frac_num: "((x::'a::{field, division_ring_inverse_zero}) / y) * z  = (x*z) / y"
    1.15    by simp
    1.16 -lemma mult_num_frac: "((x::'a::{field, division_by_zero}) / y) * z  = (x*z) / y"
    1.17 +lemma mult_num_frac: "((x::'a::{field, division_ring_inverse_zero}) / y) * z  = (x*z) / y"
    1.18    by simp
    1.19  
    1.20  lemma Numeral1_eq1_nat: "(1::nat) = Numeral1" by simp
    1.21  
    1.22 -lemma add_frac_num: "y\<noteq> 0 \<Longrightarrow> (x::'a::{field, division_by_zero}) / y + z = (x + z*y) / y"
    1.23 +lemma add_frac_num: "y\<noteq> 0 \<Longrightarrow> (x::'a::{field, division_ring_inverse_zero}) / y + z = (x + z*y) / y"
    1.24    by (simp add: add_divide_distrib)
    1.25 -lemma add_num_frac: "y\<noteq> 0 \<Longrightarrow> z + (x::'a::{field, division_by_zero}) / y = (x + z*y) / y"
    1.26 +lemma add_num_frac: "y\<noteq> 0 \<Longrightarrow> z + (x::'a::{field, division_ring_inverse_zero}) / y = (x + z*y) / y"
    1.27    by (simp add: add_divide_distrib)
    1.28  
    1.29  ML {*