src/Pure/Syntax/syntax_ext.ML
Sun, 29 Mar 2015 19:24:07 +0200 wenzelm tuned signature;
less more (0) -1 tip