src/HOL/String.thy
changeset 35115 446c5063e4fd
parent 34886 873c31d9f10d
child 35123 e286d5df187a
     1.1 --- a/src/HOL/String.thy	Thu Feb 11 22:55:16 2010 +0100
     1.2 +++ b/src/HOL/String.thy	Thu Feb 11 23:00:22 2010 +0100
     1.3 @@ -5,7 +5,7 @@
     1.4  theory String
     1.5  imports List
     1.6  uses
     1.7 -  "Tools/string_syntax.ML"
     1.8 +  ("Tools/string_syntax.ML")
     1.9    ("Tools/string_code.ML")
    1.10  begin
    1.11  
    1.12 @@ -78,6 +78,7 @@
    1.13  syntax
    1.14    "_String" :: "xstr => string"    ("_")
    1.15  
    1.16 +use "Tools/string_syntax.ML"
    1.17  setup StringSyntax.setup
    1.18  
    1.19  definition chars :: string where