src/HOL/Num.thy
changeset 48891 c0eafbd55de3
parent 47300 2284a40e0f57
child 49690 a6814de45b69
     1.1 --- a/src/HOL/Num.thy	Wed Aug 22 22:47:16 2012 +0200
     1.2 +++ b/src/HOL/Num.thy	Wed Aug 22 22:55:41 2012 +0200
     1.3 @@ -7,8 +7,6 @@
     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 @@ -333,7 +331,7 @@
    1.13      (@{const_syntax neg_numeral}, num_tr' "-")] end
    1.14  *}
    1.15  
    1.16 -use "Tools/numeral.ML"
    1.17 +ML_file "Tools/numeral.ML"
    1.18  
    1.19  
    1.20  subsection {* Class-specific numeral rules *}