2010-03-03 ago authentic syntax for classes and type constructors;
2010-03-01 ago more uniform treatment of syntax for types vs. consts;
2009-11-02 ago modernized structure Local_Syntax;
2009-09-29 ago explicit indication of Unsynchronized.ref;
2009-01-21 ago removed Ids;
2007-11-11 ago syntax operations: turned extend'' into update'' (absorb duplicates);
2007-11-10 ago update_modesyntax: based on Syntax.update_const_gram (avoids duplicates);
2007-10-11 ago renamed Syntax.XXX_mode to Syntax.mode_XXX;
2007-10-11 ago update_modesyntax: may delete 'structure' notation as well;
2007-10-10 ago replaced add_modesyntax by general update_modesyntax (add or del);
2006-09-29 ago Syntax.mode;
2006-05-16 ago added add_modesyntax;
2006-05-11 ago tuned;
2006-05-02 ago maintain implicit syntax mode;
2006-04-27 ago tuned basic list operators (flat, maps, map_filter);
2006-04-24 ago moved coalesce to AList, added equality predicates to library
2006-04-09 ago add_syntax: actually observe print mode;
2006-04-08 ago simplified handling of authentic syntax (cf. early externing in consts.ML);
2006-02-11 ago tuned mixfixes, mixfix_conflict;
2006-02-10 ago Local syntax depending on theory syntax.