src/Pure/General/ROOT.ML
2005-06-22 wenzelm 2005-06-22 removed obsolete object.ML (see Pure/library.ML);
2005-06-18 wenzelm 2005-06-18 added Pure/General/ord_list.ML;
2005-05-31 wenzelm 2005-05-31 tuned arrangement of structures;
2004-05-29 wenzelm 2004-05-29 added Pure/General/output.ML; load Pure/General/pretty.ML early in Pure/ROOT.ML;
2004-04-16 berghofe 2004-04-16 Moved symbol.ML to front of file list (due to quote function).
2003-12-05 skalberg 2003-12-05 Added lazy sequences and parser combinators for same.
2001-12-08 wenzelm 2001-12-08 use "xml.ML";
2000-06-25 wenzelm 2000-06-25 tuned;
2000-06-20 paulson 2000-06-20 new module for heaps
1999-05-15 wenzelm 1999-05-15 tuned;
1999-05-12 wenzelm 1999-05-12 added url.ML;
1999-05-11 wenzelm 1999-05-11 moved scan.ML;
1999-03-09 wenzelm 1999-03-09 added Buffer;
1999-02-04 wenzelm 1999-02-04 removed use.ML;
1999-02-03 wenzelm 1999-02-03 added use.ML;
1999-01-18 wenzelm 1999-01-18 structure Graph = Graph;
1999-01-18 wenzelm 1999-01-18 added General/graph.ML: generic direct graphs;
1999-01-13 wenzelm 1999-01-13 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
1998-11-14 wenzelm 1998-11-14 prefixed op;
1998-06-16 wenzelm 1998-06-16 added General/history.ML;
1998-06-10 wenzelm 1998-06-10 General tools.