src/Pure/General/ROOT.ML
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.