src/Pure/Syntax/simple_syntax.ML
Fri, 21 Mar 2014 20:33:56 +0100 wenzelm more qualified names;
less more (0) -10 -1 tip