src/HOL/Code_Evaluation.thy
changeset 48891 c0eafbd55de3
parent 47108 2a1953f0d20d
child 50055 94041d602ecb
     1.1 --- a/src/HOL/Code_Evaluation.thy	Wed Aug 22 22:47:16 2012 +0200
     1.2 +++ b/src/HOL/Code_Evaluation.thy	Wed Aug 22 22:55:41 2012 +0200
     1.3 @@ -6,7 +6,6 @@
     1.4  
     1.5  theory Code_Evaluation
     1.6  imports Plain Typerep Code_Numeral Predicate
     1.7 -uses ("Tools/code_evaluation.ML")
     1.8  begin
     1.9  
    1.10  subsection {* Term representation *}
    1.11 @@ -73,7 +72,7 @@
    1.12    shows "x \<equiv> y"
    1.13    using assms by simp
    1.14  
    1.15 -use "Tools/code_evaluation.ML"
    1.16 +ML_file "Tools/code_evaluation.ML"
    1.17  
    1.18  code_reserved Eval Code_Evaluation
    1.19