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