--- 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 *}
--- a/src/HOL/Num.thy Fri Mar 30 16:43:07 2012 +0200
+++ b/src/HOL/Num.thy Fri Mar 30 16:44:23 2012 +0200
@@ -7,6 +7,8 @@
theory Num
imports Datatype
+uses
+ ("Tools/numeral.ML")
begin
subsection {* The @{text num} type *}
@@ -331,6 +333,9 @@
(@{const_syntax neg_numeral}, num_tr' "-")] end
*}
+use "Tools/numeral.ML"
+
+
subsection {* Class-specific numeral rules *}
text {*