changeset 35123 | e286d5df187a |
parent 35115 | 446c5063e4fd |
child 36176 | 3fe7e97ccca8 |
--- a/src/HOL/String.thy Sat Feb 13 23:16:06 2010 +0100 +++ b/src/HOL/String.thy Sat Feb 13 23:24:57 2010 +0100 @@ -79,7 +79,7 @@ "_String" :: "xstr => string" ("_") use "Tools/string_syntax.ML" -setup StringSyntax.setup +setup String_Syntax.setup definition chars :: string where "chars = [Char Nibble0 Nibble0, Char Nibble0 Nibble1, Char Nibble0 Nibble2,