src/Pure/General/ord_list.ML
2009-10-20 haftmann 2009-10-20 replaced old_style infixes eq_set, subset, union, inter and variants by generic versions
2009-03-18 wenzelm 2009-03-18 Library.merge/OrdList.union: optimize the important special case where the tables coincide -- NOTE: this changes both the operational behaviour and the result for non-standard eq/ord notion;
2009-01-21 wenzelm 2009-01-21 removed Ids;
2008-10-16 wenzelm 2008-10-16 added make;
2008-09-25 wenzelm 2008-09-25 explicit type OrdList.T;
2007-02-26 wenzelm 2007-02-26 removed obsolete eq_set;
2005-07-19 wenzelm 2005-07-19 simplified union;
2005-07-13 wenzelm 2005-07-13 avoid excessive exceptions;
2005-07-04 wenzelm 2005-07-04 tuned union: avoid garbage in trivial case;
2005-06-22 wenzelm 2005-06-22 tuned;
2005-06-21 wenzelm 2005-06-21 added subset, eq_set; tuned insert/remove: avoid garbage;
2005-06-20 wenzelm 2005-06-20 generalized type of inter; added substract; economize heap usage;
2005-06-18 wenzelm 2005-06-18 tuned;
2005-06-18 wenzelm 2005-06-18 tuned remove;
2005-06-18 wenzelm 2005-06-18 Ordered lists without duplicates.