2011-08-24 ago more accurate treatment of index syntax constants, for proper entity references in concrete notation (e.g. infix "\<oplus>\<index>");
2011-06-09 ago tuned signature: Name.invent and Name.invent_names;
2011-06-09 ago prefer new-style Name.invents;
2011-04-08 ago more accurate markup for syntax consts, notably binders which point back to the original logical entity;
2011-04-08 ago discontinued Syntax.max_pri, which is not really a symbolic parameter;
2011-04-08 ago simplified Pure syntax bootstrap;
2011-04-08 ago renamed sprop "prop#" to "prop'" -- proper identifier;
2011-04-08 ago discontinued special treatment of structure Syntax_Ext (formerly Syn_Ext);