# HG changeset patch
# User huffman
# Date 1228883780 28800
# Node ID 8b9207f82a7808eaa1768c5565d400001821d54e
# Parent  90f42c1385853578c073f1b0b1adb4bf43b0fc9f
separate neg_simps from rel_simps

diff -r 90f42c138585 -r 8b9207f82a78 src/HOL/Groebner_Basis.thy
--- 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]
diff -r 90f42c138585 -r 8b9207f82a78 src/HOL/Int.thy
--- 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. *}
diff -r 90f42c138585 -r 8b9207f82a78 src/HOL/NatBin.thy
--- 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 *}
diff -r 90f42c138585 -r 8b9207f82a78 src/HOL/Tools/nat_simprocs.ML
--- 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;