equal
deleted
inserted
replaced
3 header {* Character and string types *} |
3 header {* Character and string types *} |
4 |
4 |
5 theory String |
5 theory String |
6 imports List |
6 imports List |
7 uses |
7 uses |
8 "Tools/string_syntax.ML" |
8 ("Tools/string_syntax.ML") |
9 ("Tools/string_code.ML") |
9 ("Tools/string_code.ML") |
10 begin |
10 begin |
11 |
11 |
12 subsection {* Characters *} |
12 subsection {* Characters *} |
13 |
13 |
76 types string = "char list" |
76 types string = "char list" |
77 |
77 |
78 syntax |
78 syntax |
79 "_String" :: "xstr => string" ("_") |
79 "_String" :: "xstr => string" ("_") |
80 |
80 |
|
81 use "Tools/string_syntax.ML" |
81 setup StringSyntax.setup |
82 setup StringSyntax.setup |
82 |
83 |
83 definition chars :: string where |
84 definition chars :: string where |
84 "chars = [Char Nibble0 Nibble0, Char Nibble0 Nibble1, Char Nibble0 Nibble2, |
85 "chars = [Char Nibble0 Nibble0, Char Nibble0 Nibble1, Char Nibble0 Nibble2, |
85 Char Nibble0 Nibble3, Char Nibble0 Nibble4, Char Nibble0 Nibble5, |
86 Char Nibble0 Nibble3, Char Nibble0 Nibble4, Char Nibble0 Nibble5, |