src/HOL/Tools/Groebner_Basis/normalizer.ML
changeset 31790 05c92381363c
parent 30866 dd5117e2d73e
child 33002 f3f02f36a3e2
     1.1 --- a/src/HOL/Tools/Groebner_Basis/normalizer.ML	Tue Jun 23 21:07:39 2009 +0200
     1.2 +++ b/src/HOL/Tools/Groebner_Basis/normalizer.ML	Wed Jun 24 09:41:14 2009 +0200
     1.3 @@ -61,7 +61,7 @@
     1.4      (HOL_basic_ss 
     1.5         addsimps @{thms arith_simps} @ natarith @ @{thms rel_simps}
     1.6               @ [if_False, if_True, @{thm add_0}, @{thm add_Suc},
     1.7 -                 @{thm add_number_of_left}, @{thm Suc_eq_add_numeral_1}]
     1.8 +                 @{thm add_number_of_left}, @{thm Suc_eq_plus1}]
     1.9               @ map (fn th => th RS sym) @{thms numerals}));
    1.10  
    1.11  val nat_mul_conv = nat_add_conv;