src/HOL/String.thy
changeset 55015 e33c5bd729ff
parent 54594 a2d1522cdd54
child 55416 dd7992d4a61a
child 55426 90f2ceed2828
     1.1 --- a/src/HOL/String.thy	Wed Jan 15 22:24:57 2014 +0100
     1.2 +++ b/src/HOL/String.thy	Wed Jan 15 23:25:28 2014 +0100
     1.3 @@ -148,7 +148,7 @@
     1.4    "Enum.enum = [Char Nibble0 Nibble0, Char Nibble0 Nibble1, Char Nibble0 Nibble2,
     1.5    Char Nibble0 Nibble3, Char Nibble0 Nibble4, Char Nibble0 Nibble5,
     1.6    Char Nibble0 Nibble6, Char Nibble0 Nibble7, Char Nibble0 Nibble8,
     1.7 -  Char Nibble0 Nibble9, Char Nibble0 NibbleA, Char Nibble0 NibbleB,
     1.8 +  Char Nibble0 Nibble9, CHR ''\<newline>'', Char Nibble0 NibbleB,
     1.9    Char Nibble0 NibbleC, Char Nibble0 NibbleD, Char Nibble0 NibbleE,
    1.10    Char Nibble0 NibbleF, Char Nibble1 Nibble0, Char Nibble1 Nibble1,
    1.11    Char Nibble1 Nibble2, Char Nibble1 Nibble3, Char Nibble1 Nibble4,