--- a/src/HOL/Groebner_Basis.thy Sun Dec 14 18:45:16 2008 +0100
+++ b/src/HOL/Groebner_Basis.thy Sun Dec 14 18:45:51 2008 +0100
@@ -163,7 +163,7 @@
end
-interpretation class_semiring: gb_semiring
+interpretation class_semiring!: gb_semiring
"op +" "op *" "op ^" "0::'a::{comm_semiring_1, recpower}" "1"
proof qed (auto simp add: ring_simps power_Suc)
@@ -242,7 +242,7 @@
end
-interpretation class_ring: gb_ring "op +" "op *" "op ^"
+interpretation class_ring!: gb_ring "op +" "op *" "op ^"
"0::'a::{comm_semiring_1,recpower,number_ring}" 1 "op -" "uminus"
proof qed simp_all
@@ -343,7 +343,7 @@
thus "b = 0" by blast
qed
-interpretation class_ringb: ringb
+interpretation class_ringb!: ringb
"op +" "op *" "op ^" "0::'a::{idom,recpower,number_ring}" "1" "op -" "uminus"
proof(unfold_locales, simp add: ring_simps power_Suc, auto)
fix w x y z ::"'a::{idom,recpower,number_ring}"
@@ -359,7 +359,7 @@
declaration {* normalizer_funs @{thm class_ringb.ringb_axioms'} *}
-interpretation natgb: semiringb
+interpretation natgb!: semiringb
"op +" "op *" "op ^" "0::nat" "1"
proof (unfold_locales, simp add: ring_simps power_Suc)
fix w x y z ::"nat"
@@ -464,7 +464,7 @@
subsection{* Groebner Bases for fields *}
-interpretation class_fieldgb:
+interpretation class_fieldgb!:
fieldgb "op +" "op *" "op ^" "0::'a::{field,recpower,number_ring}" "1" "op -" "uminus" "op /" "inverse" apply (unfold_locales) by (simp_all add: divide_inverse)
lemma divide_Numeral1: "(x::'a::{field,number_ring}) / Numeral1 = x" by simp