| Sat, 20 Aug 2011 20:00:55 +0200 |
wenzelm |
more direct balanced version Ord_List.unions;
|
file |
diff |
annotate
|
| Sat, 08 Jan 2011 17:30:05 +0100 |
wenzelm |
Ord_List.merge convenience;
|
file |
diff |
annotate
|
| Fri, 24 Sep 2010 15:53:13 +0200 |
wenzelm |
modernized structure Ord_List;
|
file |
diff |
annotate
|
| Tue, 20 Oct 2009 16:13:01 +0200 |
haftmann |
replaced old_style infixes eq_set, subset, union, inter and variants by generic versions
|
file |
diff |
annotate
|
| Wed, 18 Mar 2009 20:03:01 +0100 |
wenzelm |
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;
|
file |
diff |
annotate
|
| Wed, 21 Jan 2009 23:21:44 +0100 |
wenzelm |
removed Ids;
|
file |
diff |
annotate
|
| Thu, 16 Oct 2008 22:44:35 +0200 |
wenzelm |
added make;
|
file |
diff |
annotate
|
| Thu, 25 Sep 2008 13:21:13 +0200 |
wenzelm |
explicit type OrdList.T;
|
file |
diff |
annotate
|
| Mon, 26 Feb 2007 23:18:29 +0100 |
wenzelm |
removed obsolete eq_set;
|
file |
diff |
annotate
|
| Tue, 19 Jul 2005 17:21:58 +0200 |
wenzelm |
simplified union;
|
file |
diff |
annotate
|
| Wed, 13 Jul 2005 16:07:33 +0200 |
wenzelm |
avoid excessive exceptions;
|
file |
diff |
annotate
|
| Mon, 04 Jul 2005 17:07:14 +0200 |
wenzelm |
tuned union: avoid garbage in trivial case;
|
file |
diff |
annotate
|
| Wed, 22 Jun 2005 19:41:19 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Tue, 21 Jun 2005 09:35:31 +0200 |
wenzelm |
added subset, eq_set;
|
file |
diff |
annotate
|
| Mon, 20 Jun 2005 22:14:11 +0200 |
wenzelm |
generalized type of inter;
|
file |
diff |
annotate
|
| Sat, 18 Jun 2005 22:57:23 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Sat, 18 Jun 2005 22:47:44 +0200 |
wenzelm |
tuned remove;
|
file |
diff |
annotate
|
| Sat, 18 Jun 2005 22:40:51 +0200 |
wenzelm |
Ordered lists without duplicates.
|
file |
diff |
annotate
|