--- 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 \
--- 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" ("_")