src/HOL/String.thy
changeset 61348 d7215449be83
parent 61076 bdc1e2f0a86a
child 61799 4cf66f21b764
     1.1 --- a/src/HOL/String.thy	Tue Oct 06 21:04:44 2015 +0200
     1.2 +++ b/src/HOL/String.thy	Wed Oct 07 10:02:43 2015 +0200
     1.3 @@ -8,7 +8,7 @@
     1.4  
     1.5  subsection \<open>Characters and strings\<close>
     1.6  
     1.7 -datatype nibble =
     1.8 +datatype (plugins del: transfer) nibble =
     1.9      Nibble0 | Nibble1 | Nibble2 | Nibble3 | Nibble4 | Nibble5 | Nibble6 | Nibble7
    1.10    | Nibble8 | Nibble9 | NibbleA | NibbleB | NibbleC | NibbleD | NibbleE | NibbleF
    1.11