src/Pure/General/ROOT.ML
Sat, 07 Jul 2007 00:14:52 +0200 wenzelm added General/markup.ML;
Tue, 19 Jun 2007 23:15:43 +0200 wenzelm added General/balanced_tree.ML;
Sun, 13 May 2007 18:15:28 +0200 haftmann removed module rat.ML
Mon, 11 Dec 2006 19:05:20 +0100 wenzelm load secure.ML after symbol.ML, when default output is active;
Fri, 03 Nov 2006 14:22:43 +0100 haftmann dropped name_mangler.ML
Mon, 09 Oct 2006 19:37:03 +0200 wenzelm added General/secure.ML;
Tue, 19 Sep 2006 15:21:55 +0200 haftmann added suspensions in Pure
Mon, 12 Dec 2005 17:24:06 +0100 haftmann added generic name mangler
Wed, 09 Nov 2005 16:26:47 +0100 wenzelm tuned comments;
Fri, 14 Oct 2005 14:36:39 +0200 haftmann added module rat.ML for rational numbers
Sat, 08 Oct 2005 22:39:40 +0200 wenzelm moved susp.ML, lazy_seq.ML, lazy_scan.ML to HOL/Import;
Tue, 13 Sep 2005 22:19:30 +0200 wenzelm added stack.ML;
Sun, 28 Aug 2005 09:02:42 +0200 haftmann added alist module
Wed, 22 Jun 2005 19:41:24 +0200 wenzelm removed obsolete object.ML (see Pure/library.ML);
Sat, 18 Jun 2005 22:41:18 +0200 wenzelm added Pure/General/ord_list.ML;
Tue, 31 May 2005 11:53:27 +0200 wenzelm tuned arrangement of structures;
Sat, 29 May 2004 15:05:37 +0200 wenzelm added Pure/General/output.ML; load Pure/General/pretty.ML early in Pure/ROOT.ML;
Fri, 16 Apr 2004 18:40:21 +0200 berghofe Moved symbol.ML to front of file list (due to quote function).
Fri, 05 Dec 2003 19:39:39 +0100 skalberg Added lazy sequences and parser combinators for same.
Sat, 08 Dec 2001 14:42:22 +0100 wenzelm use "xml.ML";
Sun, 25 Jun 2000 23:45:47 +0200 wenzelm tuned;
Tue, 20 Jun 2000 11:54:22 +0200 paulson new module for heaps
Sat, 15 May 1999 16:15:54 +0200 wenzelm tuned;
Wed, 12 May 1999 16:50:56 +0200 wenzelm added url.ML;
Tue, 11 May 1999 17:51:23 +0200 wenzelm moved scan.ML;
Tue, 09 Mar 1999 12:09:05 +0100 wenzelm added Buffer;
Thu, 04 Feb 1999 18:12:26 +0100 wenzelm removed use.ML;
Wed, 03 Feb 1999 16:28:38 +0100 wenzelm added use.ML;
Mon, 18 Jan 1999 21:12:42 +0100 wenzelm structure Graph = Graph;
Mon, 18 Jan 1999 21:08:27 +0100 wenzelm added General/graph.ML: generic direct graphs;
less more (0) -30 tip