src/Pure/Syntax/local_syntax.ML
Tue, 02 Apr 2024 18:29:14 +0200 wenzelm clarified names: discontinue odd convention from 3 decades ago;
Wed, 30 Mar 2016 19:31:28 +0200 wenzelm tuned messages -- position is usually missing here;
Tue, 29 Mar 2016 21:17:29 +0200 wenzelm more position information for type mixfix;
Sun, 29 Mar 2015 19:24:07 +0200 wenzelm tuned signature;
Fri, 19 Dec 2014 17:23:56 +0100 wenzelm more frugal Local_Syntax.init -- maintain idents within context;
Sat, 25 May 2013 16:55:27 +0200 wenzelm tuned;
Sat, 25 May 2013 15:37:53 +0200 wenzelm syntax translations always depend on context;
Tue, 09 Apr 2013 13:20:09 +0200 wenzelm tuned comment;
Fri, 08 Apr 2011 16:34:14 +0200 wenzelm discontinued special treatment of structure Lexicon;
Fri, 08 Apr 2011 15:02:11 +0200 wenzelm discontinued special treatment of structure Syntax_Ext (formerly Syn_Ext);
Fri, 08 Apr 2011 13:31:16 +0200 wenzelm explicit structure Syntax_Trans;
Tue, 05 Apr 2011 15:46:35 +0200 wenzelm moved Isar/local_syntax.ML to Syntax/local_syntax.ML;
less more (0) tip