| changeset 30663 | 0b6aff7451b2 | 
| parent 28562 | 4e74209f113e | 
| child 31998 | 2c7a24f74db9 | 
--- a/src/HOL/Library/Code_Char_chr.thy Mon Mar 23 08:14:23 2009 +0100 +++ b/src/HOL/Library/Code_Char_chr.thy Mon Mar 23 08:14:24 2009 +0100 @@ -1,12 +1,11 @@ (* Title: HOL/Library/Code_Char_chr.thy - ID: $Id$ Author: Florian Haftmann *) header {* Code generation of pretty characters with character codes *} theory Code_Char_chr -imports Plain Char_nat Code_Char Code_Integer +imports Char_nat Code_Char Code_Integer Main begin definition