src/HOL/Int.thy
changeset 47228 4f4d85c3516f
parent 47226 ea712316fc87
child 47255 30a1692557b0
--- a/src/HOL/Int.thy	Fri Mar 30 16:43:07 2012 +0200
+++ b/src/HOL/Int.thy	Fri Mar 30 16:44:23 2012 +0200
@@ -8,7 +8,6 @@
 theory Int
 imports Equiv_Relations Wellfounded
 uses
-  ("Tools/numeral.ML")
   ("Tools/int_arith.ML")
 begin
 
@@ -835,7 +834,6 @@
   of_nat_0 of_nat_1 of_nat_Suc of_nat_add of_nat_mult
   of_int_0 of_int_1 of_int_add of_int_mult
 
-use "Tools/numeral.ML"
 use "Tools/int_arith.ML"
 declaration {* K Int_Arith.setup *}