src/Pure/locale.ML
Tue, 04 Aug 1998 18:21:03 +0200 wenzelm added locale.ML;
less more (0) tip