src/HOL/Groebner_Basis.thy
changeset 31068 f591144b0f17
parent 31017 2c227493ea56
child 31790 05c92381363c
     1.1 --- a/src/HOL/Groebner_Basis.thy	Fri May 08 08:01:09 2009 +0200
     1.2 +++ b/src/HOL/Groebner_Basis.thy	Fri May 08 09:48:07 2009 +0200
     1.3 @@ -635,7 +635,7 @@
     1.4  val comp_conv = (Simplifier.rewrite
     1.5  (HOL_basic_ss addsimps @{thms "Groebner_Basis.comp_arith"}
     1.6                addsimps ths addsimps simp_thms
     1.7 -              addsimprocs field_cancel_numeral_factors
     1.8 +              addsimprocs Numeral_Simprocs.field_cancel_numeral_factors
     1.9                 addsimprocs [add_frac_frac_simproc, add_frac_num_simproc,
    1.10                              ord_frac_simproc]
    1.11                  addcongs [@{thm "if_weak_cong"}]))