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