src/HOL/Num.thy

 
 header {* Binary Numerals *}
 
 theory Num
 imports Datatype
+uses
+  ("Tools/numeral.ML")
 begin
 
 subsection {* The @{text num} type *}
 
 datatype num = One | Bit0 num | Bit1 num

     end;
 in [(@{const_syntax numeral}, num_tr' ""),
     (@{const_syntax neg_numeral}, num_tr' "-")] end
 *}
 
+use "Tools/numeral.ML"
+
+
 subsection {* Class-specific numeral rules *}
 
 text {*
   @{const numeral} is a morphism.
 *}