# HG changeset patch
# User haftmann
# Date 1424296008 -3600
# Node ID aa2deef7cf47a762a8764a0c47a11629f06aa91b
# Parent  05573e5504a93023175081e18355817e70d43ae7
eliminated technical fact alias

diff -r 05573e5504a9 -r aa2deef7cf47 src/HOL/Divides.thy
--- 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}))
 )
 *}
 
diff -r 05573e5504a9 -r aa2deef7cf47 src/HOL/Int.thy
--- 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 *}
 
diff -r 05573e5504a9 -r aa2deef7cf47 src/HOL/Tools/numeral_simprocs.ML
--- 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 *)