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;
less more (0) -3 tip