src/Pure/General/ROOT.ML
Sat, 14 Nov 1998 13:26:11 +0100 wenzelm prefixed op;
Tue, 16 Jun 1998 18:37:34 +0200 wenzelm added General/history.ML;
Wed, 10 Jun 1998 11:55:30 +0200 wenzelm General tools.
less more (0) tip