# HG changeset patch
# User huffman
# Date 1333118663 -7200
# Node ID 4f4d85c3516f1cf0a0e8f893d46bdb00d318113a
# Parent  bc18fa07053b55b3cbff739f3e980691e453b2ba
load Tools/numeral.ML in Num.thy

diff -r bc18fa07053b -r 4f4d85c3516f src/HOL/Int.thy
--- 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 *}
 
diff -r bc18fa07053b -r 4f4d85c3516f src/HOL/Num.thy
--- 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 {*