src/Pure/General/ROOT.ML
2007-09-15 wenzelm 2007-09-15 added ML/ml_lex.ML;
2007-08-28 wenzelm 2007-08-28 tuned load order -- minimizes modules before Secure;
2007-08-14 wenzelm 2007-08-14 moved Tools/xml.ML to General/xml.ML (again);
2007-07-17 wenzelm 2007-07-17 added General/print_mode.ML, pure_setup.ML;
2007-07-10 wenzelm 2007-07-10 use position.ML earlier;
2007-07-09 wenzelm 2007-07-09 use position.ML after pretty.ML;
2007-07-07 wenzelm 2007-07-07 use markup.ML earlier;
2007-07-07 wenzelm 2007-07-07 moved markup.ML before position.ML;
2007-07-07 wenzelm 2007-07-07 added General/markup.ML; moved General/xml.ML to Tools/xml.ML;
2007-06-19 wenzelm 2007-06-19 added General/balanced_tree.ML;
2007-05-13 haftmann 2007-05-13 removed module rat.ML
2006-12-11 wenzelm 2006-12-11 load secure.ML after symbol.ML, when default output is active;
2006-11-03 haftmann 2006-11-03 dropped name_mangler.ML
2006-10-09 wenzelm 2006-10-09 added General/secure.ML;
2006-09-19 haftmann 2006-09-19 added suspensions in Pure
2005-12-12 haftmann 2005-12-12 added generic name mangler
2005-11-09 wenzelm 2005-11-09 tuned comments;
2005-10-14 haftmann 2005-10-14 added module rat.ML for rational numbers
2005-10-08 wenzelm 2005-10-08 moved susp.ML, lazy_seq.ML, lazy_scan.ML to HOL/Import;
2005-09-13 wenzelm 2005-09-13 added stack.ML;
2005-08-28 haftmann 2005-08-28 added alist module
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.