src/HOL/String.thy
changeset 58310 91ea607a34d8
parent 58152 6fe60a9a5bad
child 58822 90a5e981af3e
     1.1 --- a/src/HOL/String.thy	Thu Sep 11 19:26:59 2014 +0200
     1.2 +++ b/src/HOL/String.thy	Thu Sep 11 19:32:36 2014 +0200
     1.3 @@ -8,7 +8,7 @@
     1.4  
     1.5  subsection {* Characters and strings *}
     1.6  
     1.7 -datatype_new nibble =
     1.8 +datatype 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_new char = Char nibble nibble
    1.17 +datatype char = Char nibble nibble
    1.18    -- "Note: canonical order of character encoding coincides with standard term ordering"
    1.19  
    1.20  syntax