src/Pure/Thy/use.ML
Tue, 02 Dec 1997 12:40:06 +0100 wenzelm File.tmp_name;
Wed, 12 Nov 1997 16:25:45 +0100 wenzelm Redefine 'use' command in order to support path variable expansion,
less more (0) tip