src/HOL/Groebner_Basis.thy
changeset 26199 04817a8802f2
parent 26086 3c243098b64a
child 26314 9c39fc898fff
     1.1 --- a/src/HOL/Groebner_Basis.thy	Wed Mar 05 14:34:39 2008 +0100
     1.2 +++ b/src/HOL/Groebner_Basis.thy	Wed Mar 05 21:24:03 2008 +0100
     1.3 @@ -162,7 +162,7 @@
     1.4  lemma "axioms" [normalizer
     1.5      semiring ops: semiring_ops
     1.6      semiring rules: semiring_rules]:
     1.7 -  "gb_semiring add mul pwr r0 r1" by fact
     1.8 +  "gb_semiring add mul pwr r0 r1" by (rule gb_semiring_axioms)
     1.9  
    1.10  end
    1.11  
    1.12 @@ -237,7 +237,7 @@
    1.13    semiring rules: semiring_rules
    1.14    ring ops: ring_ops
    1.15    ring rules: ring_rules]:
    1.16 -  "gb_ring add mul pwr r0 r1 sub neg" by fact
    1.17 +  "gb_ring add mul pwr r0 r1 sub neg" by (rule gb_ring_axioms)
    1.18  
    1.19  end
    1.20  
    1.21 @@ -268,7 +268,7 @@
    1.22    semiring rules: semiring_rules
    1.23    ring ops: ring_ops
    1.24    ring rules: ring_rules]:
    1.25 -  "gb_field add mul pwr r0 r1 sub neg divide inverse" by fact
    1.26 +  "gb_field add mul pwr r0 r1 sub neg divide inverse" by (rule gb_field_axioms)
    1.27  
    1.28  end
    1.29  
    1.30 @@ -313,7 +313,7 @@
    1.31    semiring ops: semiring_ops
    1.32    semiring rules: semiring_rules
    1.33    idom rules: noteq_reduce add_scale_eq_noteq]:
    1.34 -  "semiringb add mul pwr r0 r1" by fact
    1.35 +  "semiringb add mul pwr r0 r1" by (rule semiringb_axioms)
    1.36  
    1.37  end
    1.38  
    1.39 @@ -330,7 +330,7 @@
    1.40    ring rules: ring_rules
    1.41    idom rules: noteq_reduce add_scale_eq_noteq
    1.42    ideal rules: subr0_iff add_r0_iff]:
    1.43 -  "ringb add mul pwr r0 r1 sub neg" by fact
    1.44 +  "ringb add mul pwr r0 r1 sub neg" by (rule ringb_axioms)
    1.45  
    1.46  end
    1.47