changeset 30663 | 0b6aff7451b2 |
parent 30224 | 79136ce06bdb |
child 36843 | ce939b5fd77b |
--- a/src/HOL/Library/Char_nat.thy Mon Mar 23 08:14:23 2009 +0100 +++ b/src/HOL/Library/Char_nat.thy Mon Mar 23 08:14:24 2009 +0100 @@ -1,12 +1,11 @@ (* Title: HOL/Library/Char_nat.thy - ID: $Id$ Author: Norbert Voelker, Florian Haftmann *) header {* Mapping between characters and natural numbers *} theory Char_nat -imports Plain "~~/src/HOL/List" +imports List Main begin text {* Conversions between nibbles and natural numbers in [0..15]. *}