src/HOL/String.thy
changeset 58822 90a5e981af3e
parent 58310 91ea607a34d8
child 58889 5b7a9633cfa8
     1.1 --- a/src/HOL/String.thy	Wed Oct 29 15:02:29 2014 +0100
     1.2 +++ b/src/HOL/String.thy	Wed Oct 29 15:07:53 2014 +0100
     1.3 @@ -126,7 +126,6 @@
     1.4    "_String" :: "str_position => string"    ("_")
     1.5  
     1.6  ML_file "Tools/string_syntax.ML"
     1.7 -setup String_Syntax.setup
     1.8  
     1.9  lemma UNIV_char:
    1.10    "UNIV = image (split Char) (UNIV \<times> UNIV)"