src/Pure/config.ML
Fri, 27 Jul 2007 16:31:14 +0200 wenzelm exported datatype value;
Wed, 25 Jul 2007 22:20:49 +0200 wenzelm Configuration options as values within the local context.
less more (0) tip