--- a/src/HOL/Divides.thy Wed Feb 18 22:46:48 2015 +0100
+++ b/src/HOL/Divides.thy Wed Feb 18 22:46:48 2015 +0100
@@ -1914,9 +1914,6 @@
text {* Tool setup *}
-(* FIXME: Theorem list add_0s doesn't exist, because Numeral0 has gone. *)
-lemmas add_0s = add_0_left add_0_right
-
ML {*
structure Cancel_Div_Mod_Int = Cancel_Div_Mod
(
@@ -1929,7 +1926,7 @@
val div_mod_eqs = map mk_meta_eq [@{thm div_mod_equality}, @{thm div_mod_equality2}];
val prove_eq_sums = Arith_Data.prove_conv2 all_tac (Arith_Data.simp_all_tac
- (@{thm diff_conv_add_uminus} :: @{thms add_0s} @ @{thms ac_simps}))
+ (@{thm diff_conv_add_uminus} :: @{thms add_0_left add_0_right} @ @{thms ac_simps}))
)
*}
--- a/src/HOL/Int.thy Wed Feb 18 22:46:48 2015 +0100
+++ b/src/HOL/Int.thy Wed Feb 18 22:46:48 2015 +0100
@@ -747,9 +747,6 @@
lemmas of_int_simps =
of_int_0 of_int_1 of_int_add of_int_mult
-lemmas int_arith_rules =
- numeral_One more_arith_simps of_nat_simps of_int_simps
-
ML_file "Tools/int_arith.ML"
declaration {* K Int_Arith.setup *}
--- a/src/HOL/Tools/numeral_simprocs.ML Wed Feb 18 22:46:48 2015 +0100
+++ b/src/HOL/Tools/numeral_simprocs.ML Wed Feb 18 22:46:48 2015 +0100
@@ -177,7 +177,7 @@
val numeral_syms = [@{thm numeral_1_eq_1} RS sym];
(*Simplify 0+n, n+0, Numeral1*n, n*Numeral1, 1*x, x*1, x/1 *)
-val add_0s = @{thms add_0s};
+val add_0s = @{thms add_0_left add_0_right};
val mult_1s = @{thms mult_1s divide_numeral_1 mult_1_left mult_1_right mult_minus1 mult_minus1_right divide_1};
(* For post-simplification of the rhs of simproc-generated rules *)