diff -r 71e99443e17d -r 1654013ec97c src/HOL/Groebner_Basis.thy
--- a/src/HOL/Groebner_Basis.thy	Mon Jun 11 16:21:03 2007 +0200
+++ b/src/HOL/Groebner_Basis.thy	Mon Jun 11 16:23:17 2007 +0200
@@ -260,6 +260,22 @@
 *} "Semiring_normalizer"
 
 
+locale gb_field = gb_ring +
+  fixes divide :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"
+    and inverse:: "'a \<Rightarrow> 'a"
+  assumes divide: "divide x y = mul x (inverse y)"
+     and inverse: "inverse x = divide r1 x"
+begin
+
+lemma "axioms" [normalizer
+  semiring ops: semiring_ops
+  semiring rules: semiring_rules
+  ring ops: ring_ops
+  ring rules: ring_rules]:
+  "gb_field add mul pwr r0 r1 sub neg divide inverse" .
+
+end
+
 subsection {* Groebner Bases *}
 
 locale semiringb = gb_semiring +
@@ -384,6 +400,21 @@
     conv = fn phi => numeral_conv}
 *}
 
+locale fieldgb = ringb + gb_field
+begin
+
+declare "axioms" [normalizer del]
+
+lemma "axioms" [normalizer
+  semiring ops: semiring_ops
+  semiring rules: semiring_rules
+  ring ops: ring_ops
+  ring rules: ring_rules
+  idom rules: noteq_reduce add_scale_eq_noteq]:
+  "fieldgb add mul pwr r0 r1 sub neg divide inverse" by unfold_locales
+end
+
+
 
 lemmas bool_simps = simp_thms(1-34)
 lemma dnf:
@@ -414,4 +445,6 @@
   Method.ctxt_args (Method.SIMPLE_METHOD' o algebra_tac)
 *} ""
 
+
+
 end