src/HOL/String.thy
changeset 58152 6fe60a9a5bad
parent 57512 cc97b347b301
child 58310 91ea607a34d8
     1.1 --- a/src/HOL/String.thy	Wed Sep 03 00:06:23 2014 +0200
     1.2 +++ b/src/HOL/String.thy	Wed Sep 03 00:06:24 2014 +0200
     1.3 @@ -8,7 +8,7 @@
     1.4  
     1.5  subsection {* Characters and strings *}
     1.6  
     1.7 -datatype nibble =
     1.8 +datatype_new nibble =
     1.9      Nibble0 | Nibble1 | Nibble2 | Nibble3 | Nibble4 | Nibble5 | Nibble6 | Nibble7
    1.10    | Nibble8 | Nibble9 | NibbleA | NibbleB | NibbleC | NibbleD | NibbleE | NibbleF
    1.11  
    1.12 @@ -114,7 +114,7 @@
    1.13    "nibble_of_nat (n mod 16) = nibble_of_nat n"
    1.14    by (simp add: nibble_of_nat_def)
    1.15  
    1.16 -datatype char = Char nibble nibble
    1.17 +datatype_new char = Char nibble nibble
    1.18    -- "Note: canonical order of character encoding coincides with standard term ordering"
    1.19  
    1.20  syntax