equal
deleted
inserted
replaced
67 "char_rec f = split f o nibble_pair_of_char" |
67 "char_rec f = split f o nibble_pair_of_char" |
68 unfolding char_case_nibble_pair [symmetric] |
68 unfolding char_case_nibble_pair [symmetric] |
69 by (simp add: fun_eq_iff split: char.split) |
69 by (simp add: fun_eq_iff split: char.split) |
70 |
70 |
71 syntax |
71 syntax |
72 "_Char" :: "xstr => char" ("CHR _") |
72 "_Char" :: "xstr_position => char" ("CHR _") |
73 |
73 |
74 |
74 |
75 subsection {* Strings *} |
75 subsection {* Strings *} |
76 |
76 |
77 type_synonym string = "char list" |
77 type_synonym string = "char list" |
78 |
78 |
79 syntax |
79 syntax |
80 "_String" :: "xstr => string" ("_") |
80 "_String" :: "xstr_position => string" ("_") |
81 |
81 |
82 use "Tools/string_syntax.ML" |
82 use "Tools/string_syntax.ML" |
83 setup String_Syntax.setup |
83 setup String_Syntax.setup |
84 |
84 |
85 definition chars :: string where |
85 definition chars :: string where |