1.1 --- a/src/HOL/Groebner_Basis.thy	Tue Dec 09 20:35:31 2008 -0800
     1.2 +++ b/src/HOL/Groebner_Basis.thy	Tue Dec 09 20:36:20 2008 -0800
     1.3 @@ -178,7 +178,8 @@
     1.4  lemma not_iszero_Numeral1: "\<not> iszero (Numeral1::'a::number_ring)"
     1.5    by (simp add: numeral_1_eq_1)
     1.6  
     1.7 -lemmas comp_arith = Let_def arith_simps nat_arith rel_simps if_False
     1.8 +lemmas comp_arith =
     1.9 +  Let_def arith_simps nat_arith rel_simps neg_simps if_False
    1.10    if_True add_0 add_Suc add_number_of_left mult_number_of_left
    1.11    numeral_1_eq_1[symmetric] Suc_eq_add_numeral_1
    1.12    numeral_0_eq_0[symmetric] numerals[symmetric]

     2.1 --- a/src/HOL/Int.thy	Tue Dec 09 20:35:31 2008 -0800
     2.2 +++ b/src/HOL/Int.thy	Tue Dec 09 20:36:20 2008 -0800
     2.3 @@ -1254,7 +1254,7 @@
     2.4    by (simp add: neg_def number_of_eq numeral_simps)
     2.5  qed
     2.6  
     2.7 -lemmas neg_simps =
     2.8 +lemmas neg_simps [simp] =
     2.9    not_neg_0 not_neg_1
    2.10    not_neg_number_of_Pls neg_number_of_Min
    2.11    neg_number_of_Bit0 neg_number_of_Bit1
    2.12 @@ -1325,7 +1325,7 @@
    2.13    less_number_of less_bin_simps
    2.14    le_number_of le_bin_simps
    2.15    eq_number_of_eq eq_bin_simps
    2.16 -  iszero_simps neg_simps
    2.17 +  iszero_simps
    2.18  
    2.19  
    2.20  subsubsection {* Simplification of arithmetic when nested to the right. *}

     3.1 --- a/src/HOL/NatBin.thy	Tue Dec 09 20:35:31 2008 -0800
     3.2 +++ b/src/HOL/NatBin.thy	Tue Dec 09 20:36:20 2008 -0800
     3.3 @@ -627,9 +627,8 @@
     3.4       {add_mono_thms = add_mono_thms, mult_mono_thms = mult_mono_thms,
     3.5        inj_thms = inj_thms,
     3.6        lessD = lessD, neqE = neqE,
     3.7 -      simpset = simpset addsimps [Suc_nat_number_of, int_nat_number_of,
     3.8 -        @{thm not_neg_number_of_Pls}, @{thm neg_number_of_Min},
     3.9 -        @{thm neg_number_of_Bit0}, @{thm neg_number_of_Bit1}]})
    3.10 +      simpset = simpset addsimps @{thms neg_simps} @
    3.11 +        [@{thm Suc_nat_number_of}, @{thm int_nat_number_of}]})
    3.12  *}
    3.13  
    3.14  declaration {* K nat_bin_arith_setup *}

     4.1 --- a/src/HOL/Tools/nat_simprocs.ML	Tue Dec 09 20:35:31 2008 -0800
     4.2 +++ b/src/HOL/Tools/nat_simprocs.ML	Tue Dec 09 20:36:20 2008 -0800
     4.3 @@ -53,7 +53,7 @@
     4.4        @{thm mult_nat_number_of}, @{thm nat_number_of_mult_left}, 
     4.5        @{thm less_nat_number_of}, 
     4.6        @{thm Let_number_of}, @{thm nat_number_of}] @
     4.7 -     @{thms arith_simps} @ @{thms rel_simps};
     4.8 +     @{thms arith_simps} @ @{thms rel_simps} @ @{thms neg_simps};
     4.9  
    4.10  fun prep_simproc (name, pats, proc) =
    4.11    Simplifier.simproc (the_context ()) name pats proc;