src/Pure/Syntax/standard_syntax.ML
Tue, 05 Apr 2011 23:14:41 +0200 wenzelm moved decode/parse operations to standard_syntax.ML;
Tue, 05 Apr 2011 18:06:45 +0200 wenzelm separate module for standard implementation of inner syntax operations;
less more (0) tip