src/Pure/General/path.ML
Thu, 03 Mar 2005 12:43:01 +0100 skalberg Move towards standard functions.
Sun, 13 Feb 2005 17:15:14 +0100 skalberg Deleted Library.option type.
Mon, 21 Jun 2004 10:25:57 +0200 kleing Merged in license change from Isabelle2004
Wed, 09 Jun 2004 18:56:55 +0200 wenzelm added split_ext; removed drop_ext;
Fri, 05 May 2000 22:02:46 +0200 wenzelm GPLed;
Tue, 26 Oct 1999 00:04:05 +0200 wenzelm added drop_ext;
Tue, 05 Oct 1999 15:26:10 +0200 wenzelm added position;
Wed, 21 Apr 1999 16:30:35 +0200 wenzelm added is_current;
Tue, 09 Mar 1999 12:09:51 +0100 wenzelm added make, dir;
Thu, 11 Feb 1999 21:15:27 +0100 wenzelm val appends: T list -> T;
Thu, 04 Feb 1999 18:13:10 +0100 wenzelm check_elem: allow ~, except for '~' and '~~';
Wed, 03 Feb 1999 16:41:49 +0100 wenzelm enabled sig;
Wed, 03 Feb 1999 16:36:38 +0100 wenzelm more abstract implementation;
Wed, 13 Jan 1999 15:18:02 +0100 wenzelm fixed titles;
Wed, 10 Jun 1998 11:51:28 +0200 wenzelm moved Thy/path.ML to General/path.ML;
less more (0) tip