equal
deleted
inserted
replaced
216 by (cases c) simp |
216 by (cases c) simp |
217 |
217 |
218 syntax |
218 syntax |
219 "_Char" :: "str_position \<Rightarrow> char" ("CHR _") |
219 "_Char" :: "str_position \<Rightarrow> char" ("CHR _") |
220 "_Char_ord" :: "num_const \<Rightarrow> char" ("CHR _") |
220 "_Char_ord" :: "num_const \<Rightarrow> char" ("CHR _") |
|
221 syntax_consts |
|
222 "_Char" "_Char_ord" \<rightleftharpoons> Char |
221 |
223 |
222 type_synonym string = "char list" |
224 type_synonym string = "char list" |
223 |
225 |
224 syntax |
226 syntax |
225 "_String" :: "str_position \<Rightarrow> string" ("_") |
227 "_String" :: "str_position \<Rightarrow> string" ("_") |
520 code_datatype "0 :: String.literal" String.Literal |
522 code_datatype "0 :: String.literal" String.Literal |
521 |
523 |
522 syntax |
524 syntax |
523 "_Literal" :: "str_position \<Rightarrow> String.literal" ("STR _") |
525 "_Literal" :: "str_position \<Rightarrow> String.literal" ("STR _") |
524 "_Ascii" :: "num_const \<Rightarrow> String.literal" ("STR _") |
526 "_Ascii" :: "num_const \<Rightarrow> String.literal" ("STR _") |
|
527 syntax_consts |
|
528 "_Literal" "_Ascii" \<rightleftharpoons> String.Literal |
525 |
529 |
526 ML_file \<open>Tools/literal.ML\<close> |
530 ML_file \<open>Tools/literal.ML\<close> |
527 |
531 |
528 |
532 |
529 subsubsection \<open>Operations\<close> |
533 subsubsection \<open>Operations\<close> |