changeset 48891 | c0eafbd55de3 |
parent 47108 | 2a1953f0d20d |
child 50055 | 94041d602ecb |
--- a/src/HOL/Code_Evaluation.thy Wed Aug 22 22:47:16 2012 +0200 +++ b/src/HOL/Code_Evaluation.thy Wed Aug 22 22:55:41 2012 +0200 @@ -6,7 +6,6 @@ theory Code_Evaluation imports Plain Typerep Code_Numeral Predicate -uses ("Tools/code_evaluation.ML") begin subsection {* Term representation *} @@ -73,7 +72,7 @@ shows "x \<equiv> y" using assms by simp -use "Tools/code_evaluation.ML" +ML_file "Tools/code_evaluation.ML" code_reserved Eval Code_Evaluation