src/Pure/Syntax/syntax_ext.ML
Sun, 29 Mar 2015 19:24:07 +0200 wenzelm tuned signature;
Fri, 31 Oct 2014 22:02:49 +0100 wenzelm discontinued obsolete \<^sync> marker;
Sat, 25 May 2013 15:37:53 +0200 wenzelm syntax translations always depend on context;
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>");
Thu, 09 Jun 2011 20:22:22 +0200 wenzelm tuned signature: Name.invent and Name.invent_names;
Thu, 09 Jun 2011 15:38:49 +0200 wenzelm prefer new-style Name.invents;
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;
less more (0) -7 tip