1.1 --- a/src/HOL/Groebner_Basis.thy	Sun Dec 14 18:45:16 2008 +0100
     1.2 +++ b/src/HOL/Groebner_Basis.thy	Sun Dec 14 18:45:51 2008 +0100
     1.3 @@ -163,7 +163,7 @@
     1.4  
     1.5  end
     1.6  
     1.7 -interpretation class_semiring: gb_semiring
     1.8 +interpretation class_semiring!: gb_semiring
     1.9      "op +" "op *" "op ^" "0::'a::{comm_semiring_1, recpower}" "1"
    1.10    proof qed (auto simp add: ring_simps power_Suc)
    1.11  
    1.12 @@ -242,7 +242,7 @@
    1.13  end
    1.14  
    1.15  
    1.16 -interpretation class_ring: gb_ring "op +" "op *" "op ^"
    1.17 +interpretation class_ring!: gb_ring "op +" "op *" "op ^"
    1.18      "0::'a::{comm_semiring_1,recpower,number_ring}" 1 "op -" "uminus"
    1.19    proof qed simp_all
    1.20  
    1.21 @@ -343,7 +343,7 @@
    1.22    thus "b = 0" by blast
    1.23  qed
    1.24  
    1.25 -interpretation class_ringb: ringb
    1.26 +interpretation class_ringb!: ringb
    1.27    "op +" "op *" "op ^" "0::'a::{idom,recpower,number_ring}" "1" "op -" "uminus"
    1.28  proof(unfold_locales, simp add: ring_simps power_Suc, auto)
    1.29    fix w x y z ::"'a::{idom,recpower,number_ring}"
    1.30 @@ -359,7 +359,7 @@
    1.31  
    1.32  declaration {* normalizer_funs @{thm class_ringb.ringb_axioms'} *}
    1.33  
    1.34 -interpretation natgb: semiringb
    1.35 +interpretation natgb!: semiringb
    1.36    "op +" "op *" "op ^" "0::nat" "1"
    1.37  proof (unfold_locales, simp add: ring_simps power_Suc)
    1.38    fix w x y z ::"nat"
    1.39 @@ -464,7 +464,7 @@
    1.40  
    1.41  subsection{* Groebner Bases for fields *}
    1.42  
    1.43 -interpretation class_fieldgb:
    1.44 +interpretation class_fieldgb!:
    1.45    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.46  
    1.47  lemma divide_Numeral1: "(x::'a::{field,number_ring}) / Numeral1 = x" by simp