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"