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"