Sun, 29 Mar 2015 19:24:07 +0200 | wenzelm | tuned signature; | file | diff | annotate |
Fri, 31 Oct 2014 22:02:49 +0100 | wenzelm | discontinued obsolete \<^sync> marker; | file | diff | annotate |
Sat, 25 May 2013 15:37:53 +0200 | wenzelm | syntax translations always depend on context; | file | diff | annotate |
Wed, 24 Aug 2011 23:00:53 +0200 | wenzelm | more accurate treatment of index syntax constants, for proper entity references in concrete notation (e.g. infix "\<oplus>\<index>"); | file | diff | annotate |
Thu, 09 Jun 2011 20:22:22 +0200 | wenzelm | tuned signature: Name.invent and Name.invent_names; | file | diff | annotate |
Thu, 09 Jun 2011 15:38:49 +0200 | wenzelm | prefer new-style Name.invents; | file | diff | annotate |
Fri, 08 Apr 2011 22:40:29 +0200 | wenzelm | more accurate markup for syntax consts, notably binders which point back to the original logical entity; | file | diff | annotate |