src/HOL/Groebner_Basis.thy
changeset 28823 dcbef866c9e2
parent 28699 32b6a8f12c1c
child 28856 5e009a80fe6d
     1.1 --- a/src/HOL/Groebner_Basis.thy	Mon Nov 17 17:00:27 2008 +0100
     1.2 +++ b/src/HOL/Groebner_Basis.thy	Mon Nov 17 17:00:55 2008 +0100
     1.3 @@ -168,7 +168,7 @@
     1.4  
     1.5  interpretation class_semiring: gb_semiring
     1.6      ["op +" "op *" "op ^" "0::'a::{comm_semiring_1, recpower}" "1"]
     1.7 -  by unfold_locales (auto simp add: ring_simps power_Suc)
     1.8 +  proof qed (auto simp add: ring_simps power_Suc)
     1.9  
    1.10  lemmas nat_arith =
    1.11    add_nat_number_of diff_nat_number_of mult_nat_number_of eq_nat_number_of less_nat_number_of
    1.12 @@ -244,7 +244,7 @@
    1.13  
    1.14  interpretation class_ring: gb_ring ["op +" "op *" "op ^"
    1.15      "0::'a::{comm_semiring_1,recpower,number_ring}" 1 "op -" "uminus"]
    1.16 -  by unfold_locales simp_all
    1.17 +  proof qed simp_all
    1.18  
    1.19  
    1.20  declaration {* normalizer_funs @{thm class_ring.gb_ring_axioms'} *}