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