src/Pure/General/ord_list.ML
Wed, 13 Jul 2005 16:07:33 +0200 wenzelm avoid excessive exceptions;
Mon, 04 Jul 2005 17:07:14 +0200 wenzelm tuned union: avoid garbage in trivial case;
Wed, 22 Jun 2005 19:41:19 +0200 wenzelm tuned;
Tue, 21 Jun 2005 09:35:31 +0200 wenzelm added subset, eq_set;
Mon, 20 Jun 2005 22:14:11 +0200 wenzelm generalized type of inter;
Sat, 18 Jun 2005 22:57:23 +0200 wenzelm tuned;
Sat, 18 Jun 2005 22:47:44 +0200 wenzelm tuned remove;
Sat, 18 Jun 2005 22:40:51 +0200 wenzelm Ordered lists without duplicates.
less more (0) tip