src/HOL/Groebner_Basis.thy
changeset 29223 e09c53289830
parent 28987 dc0ab579a5ca
child 29230 155f6c110dfc
     1.1 --- a/src/HOL/Groebner_Basis.thy	Wed Dec 10 17:19:25 2008 +0100
     1.2 +++ b/src/HOL/Groebner_Basis.thy	Thu Dec 11 18:30:26 2008 +0100
     1.3 @@ -1,5 +1,4 @@
     1.4  (*  Title:      HOL/Groebner_Basis.thy
     1.5 -    ID:         $Id$
     1.6      Author:     Amine Chaieb, TU Muenchen
     1.7  *)
     1.8  
     1.9 @@ -165,7 +164,7 @@
    1.10  end
    1.11  
    1.12  interpretation class_semiring: gb_semiring
    1.13 -    ["op +" "op *" "op ^" "0::'a::{comm_semiring_1, recpower}" "1"]
    1.14 +    "op +" "op *" "op ^" "0::'a::{comm_semiring_1, recpower}" "1"
    1.15    proof qed (auto simp add: ring_simps power_Suc)
    1.16  
    1.17  lemmas nat_arith =
    1.18 @@ -242,8 +241,8 @@
    1.19  end
    1.20  
    1.21  
    1.22 -interpretation class_ring: gb_ring ["op +" "op *" "op ^"
    1.23 -    "0::'a::{comm_semiring_1,recpower,number_ring}" 1 "op -" "uminus"]
    1.24 +interpretation class_ring: gb_ring "op +" "op *" "op ^"
    1.25 +    "0::'a::{comm_semiring_1,recpower,number_ring}" 1 "op -" "uminus"
    1.26    proof qed simp_all
    1.27  
    1.28  
    1.29 @@ -344,7 +343,7 @@
    1.30  qed
    1.31  
    1.32  interpretation class_ringb: ringb
    1.33 -  ["op +" "op *" "op ^" "0::'a::{idom,recpower,number_ring}" "1" "op -" "uminus"]
    1.34 +  "op +" "op *" "op ^" "0::'a::{idom,recpower,number_ring}" "1" "op -" "uminus"
    1.35  proof(unfold_locales, simp add: ring_simps power_Suc, auto)
    1.36    fix w x y z ::"'a::{idom,recpower,number_ring}"
    1.37    assume p: "w * y + x * z = w * z + x * y" and ynz: "y \<noteq> z"
    1.38 @@ -360,7 +359,7 @@
    1.39  declaration {* normalizer_funs @{thm class_ringb.ringb_axioms'} *}
    1.40  
    1.41  interpretation natgb: semiringb
    1.42 -  ["op +" "op *" "op ^" "0::nat" "1"]
    1.43 +  "op +" "op *" "op ^" "0::nat" "1"
    1.44  proof (unfold_locales, simp add: ring_simps power_Suc)
    1.45    fix w x y z ::"nat"
    1.46    { assume p: "w * y + x * z = w * z + x * y" and ynz: "y \<noteq> z"
    1.47 @@ -465,7 +464,7 @@
    1.48  subsection{* Groebner Bases for fields *}
    1.49  
    1.50  interpretation class_fieldgb:
    1.51 -  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.52 +  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.53  
    1.54  lemma divide_Numeral1: "(x::'a::{field,number_ring}) / Numeral1 = x" by simp
    1.55  lemma divide_Numeral0: "(x::'a::{field,number_ring, division_by_zero}) / Numeral0 = 0"