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"