2010-05-31 ago modernized some structure names, keeping a few legacy aliases;
2010-05-27 ago renamed structure PrintMode to Print_Mode, keeping the old name as legacy alias for some time;
2010-05-08 ago back-patching via Single_Assignment.var;
2010-05-03 ago renamed ProofContext.init to ProofContext.init_global to emphasize that this is not the real thing;
2010-04-19 ago update_syntax: add new productions only once, to allow repeated local notation, for example;
2010-03-09 ago simplified Syntax.basic_syntax (again);
2010-03-03 ago authentic syntax for classes and type constructors;
2010-03-01 ago more uniform treatment of syntax for types vs. consts;
2010-02-27 ago parallel brute-force disambiguation;
2010-02-21 ago filter out authentic const syntax;
2010-02-15 ago renamed InfixName to Infix etc.;
2010-02-11 ago added ML antiquotation @{syntax_const};
2009-11-25 ago normalized uncurry take/drop
2009-11-24 ago curried take/drop
2009-11-29 ago tuned message;
2009-11-08 ago adapted Generic_Data, Proof_Data;
2009-09-30 ago eliminated redundant bindings;
2009-09-29 ago explicit indication of Unsynchronized.ref;
2009-03-18 ago de-camelized Symbol_Pos;
2009-03-08 ago moved basic algebra of long names from structure NameSpace to Long_Name;
2009-03-01 ago discontinued experimental support for Alice -- too hard to maintain its many language incompatibilities, never really worked anyway;
2008-12-17 ago dropped Ids
2008-12-05 ago removed Table.extend, NameSpace.extend_table
2008-11-29 ago New lexical item "float".
2008-11-18 ago tuned;
2008-09-29 ago report_token/parse_token: back to context-less version;
2008-09-29 ago;
2008-09-26 ago eliminated polymorphic equality;
2008-08-15 ago read_asts: Lexicon.report_token, filter Lexicon.is_proper;
2008-08-10 ago added parse_token (from proof_context.ML);
2008-08-09 ago read_asts: report literal tokens;
2008-08-09 ago read_token: more robust handling of empty text;
2008-08-07 ago added read_token -- with optional YXML encoding of position;
2008-08-07 ago adapted Scan.extend_lexicon/merge_lexicons;
2008-06-18 ago TypeExt.type_constraint;
2008-06-13 ago map_const: soft version, no failure here;
2008-05-18 ago moved global pretty/string_of functions from Sign to Syntax;
2008-04-17 ago token translations: context dependent, result Pretty.T;
2008-04-16 ago tuned;
2008-04-16 ago educated guess for infix syntax
2008-01-27 ago added ambiguity_limit (restricts parse trees / terms printed in messages);
2007-11-27 ago standard_parse_term: check ambiguous results without changing the result yet;
2007-11-11 ago syntax operations: turned extend'' into update'' (absorb duplicates);
2007-11-10 ago added update_const_gram (avoids duplicates);
2007-10-20 ago moved internalM to PrintMode.internal;
2007-10-16 ago Syntax.(un)check: explicit result option;
2007-10-15 ago unparse_arity: unparse type constructor as well;
2007-10-11 ago renamed Syntax.XXX_mode to Syntax.mode_XXX;
2007-10-09 ago generic Syntax.pretty/string_of operations;
2007-09-29 ago added unparse interfaces (still unused);
2007-09-25 ago removed redundant global_parse operations;
2007-09-23 ago TypeInfer.constrain: canonical argument order;
2007-09-17 ago added print_mode_value (CRITICAL);
2007-09-01 ago added singleton check_typ/term/prop;
2007-08-30 ago turned type_check into separate typ/term_check;
2007-08-20 ago standard_parse_term: added pp/check argument, include disambig here (from sign.ML);
2007-08-20 ago type_check: tuned singleton funs case;
2007-08-14 ago renamed standard_read_XXX to standard_parse_XXX;
2007-08-14 ago added generic wrapper for parse/read functions;
2007-08-13 ago moved appl syntax to PureThy;