added Pure/General/ord_list.ML;
authorwenzelm
Sat Jun 18 22:41:18 2005 +0200 (2005-06-18)
changeset 16465eb287ce97230
parent 16464 db2711d07cd8
child 16466 82e2fc13ce54
added Pure/General/ord_list.ML;
src/Pure/General/ROOT.ML
src/Pure/IsaMakefile
     1.1 --- a/src/Pure/General/ROOT.ML	Sat Jun 18 22:40:51 2005 +0200
     1.2 +++ b/src/Pure/General/ROOT.ML	Sat Jun 18 22:41:18 2005 +0200
     1.3 @@ -4,6 +4,7 @@
     1.4  Library of general tools --- prefer this over the 'Standard ML Library'.
     1.5  *)
     1.6  
     1.7 +use "ord_list.ML";
     1.8  use "table.ML";
     1.9  use "output.ML";
    1.10  use "graph.ML";
     2.1 --- a/src/Pure/IsaMakefile	Sat Jun 18 22:40:51 2005 +0200
     2.2 +++ b/src/Pure/IsaMakefile	Sat Jun 18 22:41:18 2005 +0200
     2.3 @@ -26,7 +26,7 @@
     2.4  $(OUT)/Pure: CPure.thy General/ROOT.ML General/buffer.ML		\
     2.5    General/file.ML General/graph.ML General/heap.ML General/history.ML	\
     2.6    General/lazy_scan.ML General/lazy_seq.ML General/name_space.ML	\
     2.7 -  General/object.ML General/output.ML General/path.ML			\
     2.8 +  General/object.ML General/ord_list.ML General/output.ML General/path.ML			\
     2.9    General/position.ML General/pretty.ML General/scan.ML General/seq.ML	\
    2.10    General/source.ML General/susp.ML General/symbol.ML General/table.ML	\
    2.11    General/url.ML General/xml.ML IsaPlanner/focus_term_lib.ML		\