| changeset 46635 | cde737f9c911 |
| parent 42979 | 5b9e16259341 |
| child 46638 | fc315796794e |
--- a/src/HOL/Code_Evaluation.thy Thu Feb 23 21:16:54 2012 +0100 +++ b/src/HOL/Code_Evaluation.thy Thu Feb 23 21:25:59 2012 +0100 @@ -5,7 +5,7 @@ header {* Term evaluation using the generic code generator *} theory Code_Evaluation -imports Plain Typerep Code_Numeral +imports Plain Typerep Code_Numeral Predicate uses ("Tools/code_evaluation.ML") begin