src/Pure/Thy/use.ML
Sat, 13 Jun 1998 18:25:39 +0200 wenzelm removed use_text;
Fri, 12 Jun 1998 18:08:41 +0200 wenzelm added use_text;
Mon, 09 Mar 1998 16:13:21 +0100 wenzelm Symbol.input;
Fri, 05 Dec 1997 08:01:03 +0100 wenzelm tmp_name;
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