# HG changeset patch
# User wenzelm
# Date 1205868808 -3600
# Node ID 9c39fc898fff67b8dd38e76ca249abc1dd9795ce
# Parent  8590bf5ef343beadea140c60f46bffa22fc139ac
avoid rebinding of existing facts;

diff -r 8590bf5ef343 -r 9c39fc898fff src/HOL/Arith_Tools.thy
--- a/src/HOL/Arith_Tools.thy	Mon Mar 17 22:34:27 2008 +0100
+++ b/src/HOL/Arith_Tools.thy	Tue Mar 18 20:33:28 2008 +0100
@@ -327,24 +327,12 @@
 
 text {*Multiplying out constant divisors in comparisons (@{text "<"}, @{text "\<le>"} and @{text "="}) *}
 
-lemmas le_divide_eq_number_of = le_divide_eq [of _ _ "number_of w", standard]
-declare le_divide_eq_number_of [simp]
-
-lemmas divide_le_eq_number_of = divide_le_eq [of _ "number_of w", standard]
-declare divide_le_eq_number_of [simp]
-
-lemmas less_divide_eq_number_of = less_divide_eq [of _ _ "number_of w", standard]
-declare less_divide_eq_number_of [simp]
-
-lemmas divide_less_eq_number_of = divide_less_eq [of _ "number_of w", standard]
-declare divide_less_eq_number_of [simp]
-
-lemmas eq_divide_eq_number_of = eq_divide_eq [of _ _ "number_of w", standard]
-declare eq_divide_eq_number_of [simp]
-
-lemmas divide_eq_eq_number_of = divide_eq_eq [of _ "number_of w", standard]
-declare divide_eq_eq_number_of [simp]
-
+lemmas le_divide_eq_number_of1 [simp] = le_divide_eq [of _ _ "number_of w", standard]
+lemmas divide_le_eq_number_of1 [simp] = divide_le_eq [of _ "number_of w", standard]
+lemmas less_divide_eq_number_of1 [simp] = less_divide_eq [of _ _ "number_of w", standard]
+lemmas divide_less_eq_number_of1 [simp] = divide_less_eq [of _ "number_of w", standard]
+lemmas eq_divide_eq_number_of1 [simp] = eq_divide_eq [of _ _ "number_of w", standard]
+lemmas divide_eq_eq_number_of1 [simp] = divide_eq_eq [of _ "number_of w", standard]
 
 
 subsubsection{*Optional Simplification Rules Involving Constants*}
@@ -600,7 +588,7 @@
 in
  val field_comp_conv = comp_conv;
  val fieldgb_declaration = 
-  NormalizerData.funs @{thm class_fieldgb.axioms}
+  NormalizerData.funs @{thm class_fieldgb.fieldgb_axioms}
    {is_const = K numeral_is_const,
     dest_const = K dest_const,
     mk_const = mk_const,
diff -r 8590bf5ef343 -r 9c39fc898fff src/HOL/Groebner_Basis.thy
--- a/src/HOL/Groebner_Basis.thy	Mon Mar 17 22:34:27 2008 +0100
+++ b/src/HOL/Groebner_Basis.thy	Tue Mar 18 20:33:28 2008 +0100
@@ -159,10 +159,10 @@
 qed
 
 
-lemma "axioms" [normalizer
+lemmas gb_semiring_axioms =
+  gb_semiring_axioms [normalizer
     semiring ops: semiring_ops
-    semiring rules: semiring_rules]:
-  "gb_semiring add mul pwr r0 r1" by (rule gb_semiring_axioms)
+    semiring rules: semiring_rules]
 
 end
 
@@ -216,7 +216,7 @@
 end
 *}
 
-declaration {* normalizer_funs @{thm class_semiring.axioms} *}
+declaration {* normalizer_funs @{thm class_semiring.gb_semiring_axioms} *}
 
 
 locale gb_ring = gb_semiring +
@@ -232,12 +232,12 @@
 
 lemmas ring_rules = neg_mul sub_add
 
-lemma "axioms" [normalizer
-  semiring ops: semiring_ops
-  semiring rules: semiring_rules
-  ring ops: ring_ops
-  ring rules: ring_rules]:
-  "gb_ring add mul pwr r0 r1 sub neg" by (rule gb_ring_axioms)
+lemmas gb_ring_axioms =
+  gb_ring_axioms [normalizer
+    semiring ops: semiring_ops
+    semiring rules: semiring_rules
+    ring ops: ring_ops
+    ring rules: ring_rules]
 
 end
 
@@ -247,7 +247,7 @@
   by unfold_locales simp_all
 
 
-declaration {* normalizer_funs @{thm class_ring.axioms} *}
+declaration {* normalizer_funs @{thm class_ring.gb_ring_axioms} *}
 
 use "Tools/Groebner_Basis/normalizer.ML"
 
@@ -263,12 +263,12 @@
      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" by (rule gb_field_axioms)
+lemmas gb_field_axioms =
+  gb_field_axioms [normalizer
+    semiring ops: semiring_ops
+    semiring rules: semiring_rules
+    ring ops: ring_ops
+    ring rules: ring_rules]
 
 end
 
@@ -307,13 +307,12 @@
   thus "x = add x a \<longleftrightarrow> a = r0" by (auto simp add: add_c add_0)
 qed
 
-declare "axioms" [normalizer del]
+declare gb_semiring_axioms [normalizer del]
 
-lemma "axioms" [normalizer
+lemmas semiringb_axioms = semiringb_axioms [normalizer
   semiring ops: semiring_ops
   semiring rules: semiring_rules
-  idom rules: noteq_reduce add_scale_eq_noteq]:
-  "semiringb add mul pwr r0 r1" by (rule semiringb_axioms)
+  idom rules: noteq_reduce add_scale_eq_noteq]
 
 end
 
@@ -321,16 +320,15 @@
   assumes subr0_iff: "sub x y = r0 \<longleftrightarrow> x = y"
 begin
 
-declare "axioms" [normalizer del]
+declare gb_ring_axioms [normalizer del]
 
-lemma "axioms" [normalizer
+lemmas ringb_axioms = ringb_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
-  ideal rules: subr0_iff add_r0_iff]:
-  "ringb add mul pwr r0 r1 sub neg" by (rule ringb_axioms)
+  ideal rules: subr0_iff add_r0_iff]
 
 end
 
@@ -358,7 +356,7 @@
   thus "w = x"  by simp
 qed
 
-declaration {* normalizer_funs @{thm class_ringb.axioms} *}
+declaration {* normalizer_funs @{thm class_ringb.ringb_axioms} *}
 
 interpretation natgb: semiringb
   ["op +" "op *" "op ^" "0::nat" "1"]
@@ -382,21 +380,21 @@
   thus "(w * y + x * z = w * z + x * y) = (w = x \<or> y = z)" by auto
 qed
 
-declaration {* normalizer_funs @{thm natgb.axioms} *}
+declaration {* normalizer_funs @{thm natgb.semiringb_axioms} *}
 
 locale fieldgb = ringb + gb_field
 begin
 
-declare "axioms" [normalizer del]
+declare gb_field_axioms [normalizer del]
 
-lemma "axioms" [normalizer
+lemmas fieldgb_axioms = fieldgb_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
-  ideal rules: subr0_iff add_r0_iff]:
-  "fieldgb add mul pwr r0 r1 sub neg divide inverse" by unfold_locales
+  ideal rules: subr0_iff add_r0_iff]
+
 end