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 *}