src/HOL/Int.thy
changeset 59556 aa2deef7cf47
parent 59536 03bde055a1a0
child 59582 0fbed69ff081
     1.1 --- a/src/HOL/Int.thy	Wed Feb 18 22:46:48 2015 +0100
     1.2 +++ b/src/HOL/Int.thy	Wed Feb 18 22:46:48 2015 +0100
     1.3 @@ -747,9 +747,6 @@
     1.4  lemmas of_int_simps =
     1.5    of_int_0 of_int_1 of_int_add of_int_mult
     1.6  
     1.7 -lemmas int_arith_rules =
     1.8 -  numeral_One more_arith_simps of_nat_simps of_int_simps
     1.9 -
    1.10  ML_file "Tools/int_arith.ML"
    1.11  declaration {* K Int_Arith.setup *}
    1.12