| changeset 46664 | 1f6c140f9c72 |
| parent 46638 | fc315796794e |
| child 47108 | 2a1953f0d20d |
--- a/src/HOL/Code_Evaluation.thy Fri Feb 24 22:46:16 2012 +0100 +++ b/src/HOL/Code_Evaluation.thy Fri Feb 24 22:46:44 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