src/HOL/Groebner_Basis.thy
 changeset 31017 2c227493ea56 parent 30925 c38cbc0ac8d1 child 31068 f591144b0f17
```     1.1 --- a/src/HOL/Groebner_Basis.thy	Tue Apr 28 15:50:30 2009 +0200
1.2 +++ b/src/HOL/Groebner_Basis.thy	Tue Apr 28 15:50:30 2009 +0200
1.3 @@ -164,7 +164,7 @@
1.4  end
1.5
1.6  interpretation class_semiring: gb_semiring
1.7 -    "op +" "op *" "op ^" "0::'a::{comm_semiring_1, recpower}" "1"
1.8 +    "op +" "op *" "op ^" "0::'a::{comm_semiring_1}" "1"
1.9    proof qed (auto simp add: algebra_simps power_Suc)
1.10
1.11  lemmas nat_arith =
1.12 @@ -242,7 +242,7 @@
1.13
1.14
1.15  interpretation class_ring: gb_ring "op +" "op *" "op ^"
1.16 -    "0::'a::{comm_semiring_1,recpower,number_ring}" 1 "op -" "uminus"
1.17 +    "0::'a::{comm_semiring_1,number_ring}" 1 "op -" "uminus"
1.18    proof qed simp_all
1.19
1.20
1.21 @@ -349,9 +349,9 @@
1.22  qed
1.23
1.24  interpretation class_ringb: ringb
1.25 -  "op +" "op *" "op ^" "0::'a::{idom,recpower,number_ring}" "1" "op -" "uminus"
1.26 +  "op +" "op *" "op ^" "0::'a::{idom,number_ring}" "1" "op -" "uminus"
1.27  proof(unfold_locales, simp add: algebra_simps power_Suc, auto)
1.28 -  fix w x y z ::"'a::{idom,recpower,number_ring}"
1.29 +  fix w x y z ::"'a::{idom,number_ring}"
1.30    assume p: "w * y + x * z = w * z + x * y" and ynz: "y \<noteq> z"
1.31    hence ynz': "y - z \<noteq> 0" by simp
1.32    from p have "w * y + x* z - w*z - x*y = 0" by simp
1.33 @@ -471,7 +471,7 @@
1.34  subsection{* Groebner Bases for fields *}
1.35
1.36  interpretation class_fieldgb:
1.37 -  fieldgb "op +" "op *" "op ^" "0::'a::{field,recpower,number_ring}" "1" "op -" "uminus" "op /" "inverse" apply (unfold_locales) by (simp_all add: divide_inverse)
1.38 +  fieldgb "op +" "op *" "op ^" "0::'a::{field,number_ring}" "1" "op -" "uminus" "op /" "inverse" apply (unfold_locales) by (simp_all add: divide_inverse)
1.39
1.40  lemma divide_Numeral1: "(x::'a::{field,number_ring}) / Numeral1 = x" by simp
1.41  lemma divide_Numeral0: "(x::'a::{field,number_ring, division_by_zero}) / Numeral0 = 0"
```