src/HOL/String.thy
changeset 46483 10a9c31a22b4
parent 45490 20c8c0cca555
child 48891 c0eafbd55de3
     1.1 --- a/src/HOL/String.thy	Tue Feb 14 22:48:07 2012 +0100
     1.2 +++ b/src/HOL/String.thy	Wed Feb 15 13:24:22 2012 +0100
     1.3 @@ -69,7 +69,7 @@
     1.4    by (simp add: fun_eq_iff split: char.split)
     1.5  
     1.6  syntax
     1.7 -  "_Char" :: "xstr_position => char"    ("CHR _")
     1.8 +  "_Char" :: "str_position => char"    ("CHR _")
     1.9  
    1.10  
    1.11  subsection {* Strings *}
    1.12 @@ -77,7 +77,7 @@
    1.13  type_synonym string = "char list"
    1.14  
    1.15  syntax
    1.16 -  "_String" :: "xstr_position => string"    ("_")
    1.17 +  "_String" :: "str_position => string"    ("_")
    1.18  
    1.19  use "Tools/string_syntax.ML"
    1.20  setup String_Syntax.setup