# HG changeset patch
# User wenzelm
# Date 1183586771 -7200
# Node ID 42765aff66d6c1685bd2c4240c7b2f44ff56cdbb
# Parent  d85a277f90fd59c332126720ce4621628c61e7dc
added Tools/numeral.ML;

diff -r d85a277f90fd -r 42765aff66d6 src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Thu Jul 05 00:06:10 2007 +0200
+++ b/src/HOL/IsaMakefile	Thu Jul 05 00:06:11 2007 +0200
@@ -116,10 +116,9 @@
   Tools/function_package/inductive_wrap.ML				\
   Tools/function_package/lexicographic_order.ML				\
   Tools/function_package/mutual.ML					\
-  Tools/function_package/pattern_split.ML				\
-  Tools/inductive_codegen.ML	\
+  Tools/function_package/pattern_split.ML Tools/inductive_codegen.ML	\
   Tools/inductive_package.ML Tools/inductive_realizer.ML Tools/meson.ML	\
-  Tools/metis_tools.ML Tools/numeral_syntax.ML 				\
+  Tools/metis_tools.ML Tools/numeral.ML Tools/numeral_syntax.ML		\
   Tools/old_inductive_package.ML Tools/polyhash.ML 			\
   Tools/primrec_package.ML Tools/prop_logic.ML 	\
   Tools/recdef_package.ML Tools/recfun_codegen.ML			\
diff -r d85a277f90fd -r 42765aff66d6 src/HOL/Numeral.thy
--- a/src/HOL/Numeral.thy	Thu Jul 05 00:06:10 2007 +0200
+++ b/src/HOL/Numeral.thy	Thu Jul 05 00:06:11 2007 +0200
@@ -8,7 +8,9 @@
 
 theory Numeral
 imports IntDef
-uses ("Tools/numeral_syntax.ML")
+uses
+  ("Tools/numeral.ML")
+  ("Tools/numeral_syntax.ML")
 begin
 
 subsection {* Binary representation *}
@@ -47,6 +49,8 @@
 class number = type + -- {* for numeric types: nat, int, real, \dots *}
   fixes number_of :: "int \<Rightarrow> 'a"
 
+use "Tools/numeral.ML"
+
 syntax
   "_Numeral" :: "num_const \<Rightarrow> 'a"    ("_")