--- a/src/HOL/Groebner_Basis.thy Tue Dec 09 20:35:31 2008 -0800
+++ b/src/HOL/Groebner_Basis.thy Tue Dec 09 20:36:20 2008 -0800
@@ -178,7 +178,8 @@
lemma not_iszero_Numeral1: "\<not> iszero (Numeral1::'a::number_ring)"
by (simp add: numeral_1_eq_1)
-lemmas comp_arith = Let_def arith_simps nat_arith rel_simps if_False
+lemmas comp_arith =
+ Let_def arith_simps nat_arith rel_simps neg_simps if_False
if_True add_0 add_Suc add_number_of_left mult_number_of_left
numeral_1_eq_1[symmetric] Suc_eq_add_numeral_1
numeral_0_eq_0[symmetric] numerals[symmetric]
--- a/src/HOL/Int.thy Tue Dec 09 20:35:31 2008 -0800
+++ b/src/HOL/Int.thy Tue Dec 09 20:36:20 2008 -0800
@@ -1254,7 +1254,7 @@
by (simp add: neg_def number_of_eq numeral_simps)
qed
-lemmas neg_simps =
+lemmas neg_simps [simp] =
not_neg_0 not_neg_1
not_neg_number_of_Pls neg_number_of_Min
neg_number_of_Bit0 neg_number_of_Bit1
@@ -1325,7 +1325,7 @@
less_number_of less_bin_simps
le_number_of le_bin_simps
eq_number_of_eq eq_bin_simps
- iszero_simps neg_simps
+ iszero_simps
subsubsection {* Simplification of arithmetic when nested to the right. *}
--- a/src/HOL/NatBin.thy Tue Dec 09 20:35:31 2008 -0800
+++ b/src/HOL/NatBin.thy Tue Dec 09 20:36:20 2008 -0800
@@ -627,9 +627,8 @@
{add_mono_thms = add_mono_thms, mult_mono_thms = mult_mono_thms,
inj_thms = inj_thms,
lessD = lessD, neqE = neqE,
- simpset = simpset addsimps [Suc_nat_number_of, int_nat_number_of,
- @{thm not_neg_number_of_Pls}, @{thm neg_number_of_Min},
- @{thm neg_number_of_Bit0}, @{thm neg_number_of_Bit1}]})
+ simpset = simpset addsimps @{thms neg_simps} @
+ [@{thm Suc_nat_number_of}, @{thm int_nat_number_of}]})
*}
declaration {* K nat_bin_arith_setup *}
--- a/src/HOL/Tools/nat_simprocs.ML Tue Dec 09 20:35:31 2008 -0800
+++ b/src/HOL/Tools/nat_simprocs.ML Tue Dec 09 20:36:20 2008 -0800
@@ -53,7 +53,7 @@
@{thm mult_nat_number_of}, @{thm nat_number_of_mult_left},
@{thm less_nat_number_of},
@{thm Let_number_of}, @{thm nat_number_of}] @
- @{thms arith_simps} @ @{thms rel_simps};
+ @{thms arith_simps} @ @{thms rel_simps} @ @{thms neg_simps};
fun prep_simproc (name, pats, proc) =
Simplifier.simproc (the_context ()) name pats proc;