src/HOL/Int.thy
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 *}