src/HOL/Int.thy

--- a/src/HOL/Int.thy	Mon Nov 04 18:08:47 2013 +0100
+++ b/src/HOL/Int.thy	Mon Nov 04 20:10:06 2013 +0100
@@ -424,6 +424,11 @@
 
 end
 
+lemma diff_nat_numeral [simp]: 
+  "(numeral v :: nat) - numeral v' = nat (numeral v - numeral v')"
+  by (simp only: nat_diff_distrib' zero_le_numeral nat_numeral)
+
+
 text {* For termination proofs: *}
 lemma measure_function_int[measure_function]: "is_measure (nat o abs)" ..
 
@@ -747,14 +752,11 @@
 
 subsection {* Setting up simplification procedures *}
 
+lemmas of_int_simps =
+  of_int_0 of_int_1 of_int_add of_int_mult
+
 lemmas int_arith_rules =
-  neg_le_iff_le numeral_One
-  minus_zero left_minus right_minus
-  mult_zero_left mult_zero_right mult_1_left mult_1_right
-  mult_minus_left mult_minus_right
-  minus_add_distrib minus_minus mult_assoc
-  of_nat_0 of_nat_1 of_nat_Suc of_nat_add of_nat_mult
-  of_int_0 of_int_1 of_int_add of_int_mult
+  numeral_One more_arith_simps of_nat_simps of_int_simps
 
 ML_file "Tools/int_arith.ML"
 declaration {* K Int_Arith.setup *}
@@ -875,16 +877,10 @@
               if d < 0 then 0 else nat d)"
 by (simp add: Let_def nat_diff_distrib [symmetric])
 
-lemma diff_nat_numeral [simp]: 
-  "(numeral v :: nat) - numeral v' = nat (numeral v - numeral v')"
-  by (simp only: nat_diff_distrib' zero_le_numeral nat_numeral)
-
 lemma nat_numeral_diff_1 [simp]:
   "numeral v - (1::nat) = nat (numeral v - 1)"
   using diff_nat_numeral [of v Num.One] by simp
 
-lemmas nat_arith = diff_nat_numeral
-
 
 subsection "Induction principles for int"