src/HOL/Tools/string_syntax.ML
2012-02-15 wenzelm 2012-02-15 renamed "xstr" to "str_token";
2011-11-14 wenzelm 2011-11-14 inner syntax positions for string literals;
2011-04-08 wenzelm 2011-04-08 discontinued special treatment of structure Lexicon;
2011-04-06 wenzelm 2011-04-06 discontinued old-style Syntax.constrainC;
2011-04-05 wenzelm 2011-04-05 discontinued special treatment of structure Ast: no pervasive content, no inclusion in structure Syntax;
2010-11-20 wenzelm 2010-11-20 renamed raw "explode" function to "raw_explode" to emphasize its meaning;
2010-02-25 wenzelm 2010-02-25 explicit @{type_syntax} markup;
2010-02-21 wenzelm 2010-02-21 slightly more abstract syntax mark/unmark operations;
2010-02-21 wenzelm 2010-02-21 adapted to authentic syntax;
2010-02-13 wenzelm 2010-02-13 modernized structures;
2010-02-11 wenzelm 2010-02-11 modernized translations; formal markup of @{syntax_const} and @{const_syntax}; minor tuning;
2009-05-06 haftmann 2009-05-06 refined HOL string theories and corresponding ML fragments
2009-01-02 wenzelm 2009-01-02 renamed token markup "_xstr" to "_inner_string";
2007-09-25 wenzelm 2007-09-25 proper Sign operations instead of Theory aliases;
2006-12-11 wenzelm 2006-12-11 specials: include single quote;
2006-12-10 wenzelm 2006-12-10 Concrete syntax for hex chars and strings.
2000-12-23 wenzelm 2000-12-23 Tools/string_syntax.ML;