avoid rebinding of existing facts;
authorwenzelm
Fri Mar 28 19:43:54 2008 +0100 (2008-03-28)
changeset 26462dac4e2bce00d
parent 26461 da989545e59c
child 26463 9283b4185fdf
avoid rebinding of existing facts;
src/HOL/Arith_Tools.thy
src/HOL/Groebner_Basis.thy
     1.1 --- a/src/HOL/Arith_Tools.thy	Fri Mar 28 19:12:39 2008 +0100
     1.2 +++ b/src/HOL/Arith_Tools.thy	Fri Mar 28 19:43:54 2008 +0100
     1.3 @@ -588,7 +588,7 @@
     1.4  in
     1.5   val field_comp_conv = comp_conv;
     1.6   val fieldgb_declaration = 
     1.7 -  NormalizerData.funs @{thm class_fieldgb.fieldgb_axioms}
     1.8 +  NormalizerData.funs @{thm class_fieldgb.fieldgb_axioms'}
     1.9     {is_const = K numeral_is_const,
    1.10      dest_const = K dest_const,
    1.11      mk_const = mk_const,
     2.1 --- a/src/HOL/Groebner_Basis.thy	Fri Mar 28 19:12:39 2008 +0100
     2.2 +++ b/src/HOL/Groebner_Basis.thy	Fri Mar 28 19:43:54 2008 +0100
     2.3 @@ -159,7 +159,7 @@
     2.4  qed
     2.5  
     2.6  
     2.7 -lemmas gb_semiring_axioms =
     2.8 +lemmas gb_semiring_axioms' =
     2.9    gb_semiring_axioms [normalizer
    2.10      semiring ops: semiring_ops
    2.11      semiring rules: semiring_rules]
    2.12 @@ -216,7 +216,7 @@
    2.13  end
    2.14  *}
    2.15  
    2.16 -declaration {* normalizer_funs @{thm class_semiring.gb_semiring_axioms} *}
    2.17 +declaration {* normalizer_funs @{thm class_semiring.gb_semiring_axioms'} *}
    2.18  
    2.19  
    2.20  locale gb_ring = gb_semiring +
    2.21 @@ -232,7 +232,7 @@
    2.22  
    2.23  lemmas ring_rules = neg_mul sub_add
    2.24  
    2.25 -lemmas gb_ring_axioms =
    2.26 +lemmas gb_ring_axioms' =
    2.27    gb_ring_axioms [normalizer
    2.28      semiring ops: semiring_ops
    2.29      semiring rules: semiring_rules
    2.30 @@ -247,7 +247,7 @@
    2.31    by unfold_locales simp_all
    2.32  
    2.33  
    2.34 -declaration {* normalizer_funs @{thm class_ring.gb_ring_axioms} *}
    2.35 +declaration {* normalizer_funs @{thm class_ring.gb_ring_axioms'} *}
    2.36  
    2.37  use "Tools/Groebner_Basis/normalizer.ML"
    2.38  
    2.39 @@ -263,7 +263,7 @@
    2.40       and inverse: "inverse x = divide r1 x"
    2.41  begin
    2.42  
    2.43 -lemmas gb_field_axioms =
    2.44 +lemmas gb_field_axioms' =
    2.45    gb_field_axioms [normalizer
    2.46      semiring ops: semiring_ops
    2.47      semiring rules: semiring_rules
    2.48 @@ -307,9 +307,9 @@
    2.49    thus "x = add x a \<longleftrightarrow> a = r0" by (auto simp add: add_c add_0)
    2.50  qed
    2.51  
    2.52 -declare gb_semiring_axioms [normalizer del]
    2.53 +declare gb_semiring_axioms' [normalizer del]
    2.54  
    2.55 -lemmas semiringb_axioms = semiringb_axioms [normalizer
    2.56 +lemmas semiringb_axioms' = semiringb_axioms [normalizer
    2.57    semiring ops: semiring_ops
    2.58    semiring rules: semiring_rules
    2.59    idom rules: noteq_reduce add_scale_eq_noteq]
    2.60 @@ -320,9 +320,9 @@
    2.61    assumes subr0_iff: "sub x y = r0 \<longleftrightarrow> x = y"
    2.62  begin
    2.63  
    2.64 -declare gb_ring_axioms [normalizer del]
    2.65 +declare gb_ring_axioms' [normalizer del]
    2.66  
    2.67 -lemmas ringb_axioms = ringb_axioms [normalizer
    2.68 +lemmas ringb_axioms' = ringb_axioms [normalizer
    2.69    semiring ops: semiring_ops
    2.70    semiring rules: semiring_rules
    2.71    ring ops: ring_ops
    2.72 @@ -356,7 +356,7 @@
    2.73    thus "w = x"  by simp
    2.74  qed
    2.75  
    2.76 -declaration {* normalizer_funs @{thm class_ringb.ringb_axioms} *}
    2.77 +declaration {* normalizer_funs @{thm class_ringb.ringb_axioms'} *}
    2.78  
    2.79  interpretation natgb: semiringb
    2.80    ["op +" "op *" "op ^" "0::nat" "1"]
    2.81 @@ -380,14 +380,14 @@
    2.82    thus "(w * y + x * z = w * z + x * y) = (w = x \<or> y = z)" by auto
    2.83  qed
    2.84  
    2.85 -declaration {* normalizer_funs @{thm natgb.semiringb_axioms} *}
    2.86 +declaration {* normalizer_funs @{thm natgb.semiringb_axioms'} *}
    2.87  
    2.88  locale fieldgb = ringb + gb_field
    2.89  begin
    2.90  
    2.91 -declare gb_field_axioms [normalizer del]
    2.92 +declare gb_field_axioms' [normalizer del]
    2.93  
    2.94 -lemmas fieldgb_axioms = fieldgb_axioms [normalizer
    2.95 +lemmas fieldgb_axioms' = fieldgb_axioms [normalizer
    2.96    semiring ops: semiring_ops
    2.97    semiring rules: semiring_rules
    2.98    ring ops: ring_ops