| changeset 28313 | 1742947952f8 |
| parent 28243 | 84d90ec67059 |
| child 28335 | 25326092cf9a |
--- a/src/HOL/Code_Eval.thy Mon Sep 22 13:55:59 2008 +0200 +++ b/src/HOL/Code_Eval.thy Mon Sep 22 13:56:01 2008 +0200 @@ -6,7 +6,7 @@ header {* Term evaluation using the generic code generator *} theory Code_Eval -imports Plain RType +imports Plain "~~/src/HOL/Library/RType" begin subsection {* Term representation *}