src/HOL/Groebner_Basis.thy
changeset 26462 dac4e2bce00d
parent 26314 9c39fc898fff
child 27666 1436d81d1294
     1.1 --- a/src/HOL/Groebner_Basis.thy	Fri Mar 28 19:12:39 2008 +0100
     1.2 +++ b/src/HOL/Groebner_Basis.thy	Fri Mar 28 19:43:54 2008 +0100
     1.3 @@ -159,7 +159,7 @@
     1.4  qed
     1.5  
     1.6  
     1.7 -lemmas gb_semiring_axioms =
     1.8 +lemmas gb_semiring_axioms' =
     1.9    gb_semiring_axioms [normalizer
    1.10      semiring ops: semiring_ops
    1.11      semiring rules: semiring_rules]
    1.12 @@ -216,7 +216,7 @@
    1.13  end
    1.14  *}
    1.15  
    1.16 -declaration {* normalizer_funs @{thm class_semiring.gb_semiring_axioms} *}
    1.17 +declaration {* normalizer_funs @{thm class_semiring.gb_semiring_axioms'} *}
    1.18  
    1.19  
    1.20  locale gb_ring = gb_semiring +
    1.21 @@ -232,7 +232,7 @@
    1.22  
    1.23  lemmas ring_rules = neg_mul sub_add
    1.24  
    1.25 -lemmas gb_ring_axioms =
    1.26 +lemmas gb_ring_axioms' =
    1.27    gb_ring_axioms [normalizer
    1.28      semiring ops: semiring_ops
    1.29      semiring rules: semiring_rules
    1.30 @@ -247,7 +247,7 @@
    1.31    by unfold_locales simp_all
    1.32  
    1.33  
    1.34 -declaration {* normalizer_funs @{thm class_ring.gb_ring_axioms} *}
    1.35 +declaration {* normalizer_funs @{thm class_ring.gb_ring_axioms'} *}
    1.36  
    1.37  use "Tools/Groebner_Basis/normalizer.ML"
    1.38  
    1.39 @@ -263,7 +263,7 @@
    1.40       and inverse: "inverse x = divide r1 x"
    1.41  begin
    1.42  
    1.43 -lemmas gb_field_axioms =
    1.44 +lemmas gb_field_axioms' =
    1.45    gb_field_axioms [normalizer
    1.46      semiring ops: semiring_ops
    1.47      semiring rules: semiring_rules
    1.48 @@ -307,9 +307,9 @@
    1.49    thus "x = add x a \<longleftrightarrow> a = r0" by (auto simp add: add_c add_0)
    1.50  qed
    1.51  
    1.52 -declare gb_semiring_axioms [normalizer del]
    1.53 +declare gb_semiring_axioms' [normalizer del]
    1.54  
    1.55 -lemmas semiringb_axioms = semiringb_axioms [normalizer
    1.56 +lemmas semiringb_axioms' = semiringb_axioms [normalizer
    1.57    semiring ops: semiring_ops
    1.58    semiring rules: semiring_rules
    1.59    idom rules: noteq_reduce add_scale_eq_noteq]
    1.60 @@ -320,9 +320,9 @@
    1.61    assumes subr0_iff: "sub x y = r0 \<longleftrightarrow> x = y"
    1.62  begin
    1.63  
    1.64 -declare gb_ring_axioms [normalizer del]
    1.65 +declare gb_ring_axioms' [normalizer del]
    1.66  
    1.67 -lemmas ringb_axioms = ringb_axioms [normalizer
    1.68 +lemmas ringb_axioms' = ringb_axioms [normalizer
    1.69    semiring ops: semiring_ops
    1.70    semiring rules: semiring_rules
    1.71    ring ops: ring_ops
    1.72 @@ -356,7 +356,7 @@
    1.73    thus "w = x"  by simp
    1.74  qed
    1.75  
    1.76 -declaration {* normalizer_funs @{thm class_ringb.ringb_axioms} *}
    1.77 +declaration {* normalizer_funs @{thm class_ringb.ringb_axioms'} *}
    1.78  
    1.79  interpretation natgb: semiringb
    1.80    ["op +" "op *" "op ^" "0::nat" "1"]
    1.81 @@ -380,14 +380,14 @@
    1.82    thus "(w * y + x * z = w * z + x * y) = (w = x \<or> y = z)" by auto
    1.83  qed
    1.84  
    1.85 -declaration {* normalizer_funs @{thm natgb.semiringb_axioms} *}
    1.86 +declaration {* normalizer_funs @{thm natgb.semiringb_axioms'} *}
    1.87  
    1.88  locale fieldgb = ringb + gb_field
    1.89  begin
    1.90  
    1.91 -declare gb_field_axioms [normalizer del]
    1.92 +declare gb_field_axioms' [normalizer del]
    1.93  
    1.94 -lemmas fieldgb_axioms = fieldgb_axioms [normalizer
    1.95 +lemmas fieldgb_axioms' = fieldgb_axioms [normalizer
    1.96    semiring ops: semiring_ops
    1.97    semiring rules: semiring_rules
    1.98    ring ops: ring_ops