| changeset 27368 | 9f90ac19e32b | 
| parent 24999 | 1dbe785ed529 | 
| child 28562 | 4e74209f113e | 
--- a/src/HOL/Library/Code_Char_chr.thy Thu Jun 26 10:06:54 2008 +0200 +++ b/src/HOL/Library/Code_Char_chr.thy Thu Jun 26 10:07:01 2008 +0200 @@ -6,7 +6,7 @@ header {* Code generation of pretty characters with character codes *} theory Code_Char_chr -imports Char_nat Code_Char Code_Integer +imports Plain Char_nat Code_Char Code_Integer begin definition