changeset 59556 | aa2deef7cf47 |
parent 59536 | 03bde055a1a0 |
child 59582 | 0fbed69ff081 |
--- 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 *}