src/HOL/Num.thy
changeset 47228 4f4d85c3516f
parent 47227 bc18fa07053b
child 47255 30a1692557b0
     1.1 --- a/src/HOL/Num.thy	Fri Mar 30 16:43:07 2012 +0200
     1.2 +++ b/src/HOL/Num.thy	Fri Mar 30 16:44:23 2012 +0200
     1.3 @@ -7,6 +7,8 @@
     1.4  
     1.5  theory Num
     1.6  imports Datatype
     1.7 +uses
     1.8 +  ("Tools/numeral.ML")
     1.9  begin
    1.10  
    1.11  subsection {* The @{text num} type *}
    1.12 @@ -331,6 +333,9 @@
    1.13      (@{const_syntax neg_numeral}, num_tr' "-")] end
    1.14  *}
    1.15  
    1.16 +use "Tools/numeral.ML"
    1.17 +
    1.18 +
    1.19  subsection {* Class-specific numeral rules *}
    1.20  
    1.21  text {*