| Thu, 07 Mar 2013 15:02:55 +0100 |
wenzelm |
tuned signature -- prefer terminology of Scala and Axiom;
|
file |
diff |
annotate
|
| Wed, 16 Jan 2013 20:40:50 +0100 |
wenzelm |
eliminated dead code;
|
file |
diff |
annotate
|
| Sun, 30 Dec 2012 16:33:05 +0100 |
wenzelm |
tuned whitespace;
|
file |
diff |
annotate
|
| Thu, 23 Aug 2012 13:03:29 +0200 |
wenzelm |
prefer classic take_prefix/take_suffix over chop_while (cf. 0659e84bdc5f);
|
file |
diff |
annotate
|
| Mon, 16 Jul 2012 15:57:21 +0200 |
wenzelm |
replaced quicksort by mergesort, which might be a bit more efficient for key operations like Ord_List.make, Sorts.minimize_sort;
|
file |
diff |
annotate
|
| Mon, 16 Apr 2012 23:07:40 +0200 |
wenzelm |
redirect bash stderr to Isabelle warning as appropriate -- avoid raw process error output which may either get ignored or overload PIDE syslog in extreme cases;
|
file |
diff |
annotate
|
| Wed, 21 Mar 2012 11:00:34 +0100 |
wenzelm |
prefer explicitly qualified exception List.Empty;
|
file |
diff |
annotate
|
| Mon, 19 Mar 2012 21:16:19 +0100 |
wenzelm |
discontinued remains of duplicate exception UnequalLengths (cf. 441260986b63);
|
file |
diff |
annotate
|
| Mon, 19 Mar 2012 21:10:33 +0100 |
wenzelm |
moved some legacy stuff;
|
file |
diff |
annotate
|
| Mon, 12 Mar 2012 23:16:02 +0100 |
wenzelm |
some support for grouped list operations;
|
file |
diff |
annotate
|
| Thu, 08 Mar 2012 21:35:54 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Sat, 03 Mar 2012 22:27:30 +0100 |
wenzelm |
discontinued obsolete Library.foldl_map and Library.apply (NB: apply = fold I);
|
file |
diff |
annotate
|
| Thu, 24 Nov 2011 21:15:20 +0100 |
wenzelm |
more abstract datatype stamp, which avoids pointless allocation of mutable cells;
|
file |
diff |
annotate
|
| Thu, 01 Sep 2011 14:10:52 +0200 |
wenzelm |
more flexible sorting;
|
file |
diff |
annotate
|
| Wed, 13 Jul 2011 20:13:27 +0200 |
wenzelm |
low-level tuning;
|
file |
diff |
annotate
|
| Mon, 04 Jul 2011 16:51:45 +0200 |
wenzelm |
pervasive Basic_Library in Scala;
|
file |
diff |
annotate
|
| Thu, 30 Jun 2011 13:59:55 +0200 |
wenzelm |
getenv_strict in ML;
|
file |
diff |
annotate
|
| Mon, 27 Jun 2011 15:03:55 +0200 |
wenzelm |
old gensym is now legacy -- global state is out of fashion, and its result is not guaranteed to be fresh;
|
file |
diff |
annotate
|
| Wed, 08 Jun 2011 15:56:57 +0200 |
wenzelm |
more robust exception pattern General.Subscript;
|
file |
diff |
annotate
|
| Tue, 19 Apr 2011 15:58:05 +0200 |
wenzelm |
slightly more special eq_list/eq_set, with shortcut involving pointer_eq;
|
file |
diff |
annotate
|
| Wed, 12 Jan 2011 14:07:29 +0100 |
wenzelm |
smart_string_of_real: print integer values without fractional part;
|
file |
diff |
annotate
|
| Mon, 10 Jan 2011 16:56:47 +0100 |
wenzelm |
made SML/NJ happy;
|
file |
diff |
annotate
|
| Mon, 10 Jan 2011 16:07:16 +0100 |
wenzelm |
tuned string_of_int to avoid allocation for small integers;
|
file |
diff |
annotate
|
| Mon, 10 Jan 2011 15:19:48 +0100 |
wenzelm |
standardized split_last/last_elem towards List.last;
|
file |
diff |
annotate
|
| Fri, 03 Dec 2010 17:29:27 +0100 |
wenzelm |
removed confusing comments (cf. 500171e7aa59);
|
file |
diff |
annotate
|
| Fri, 03 Dec 2010 10:17:55 +0100 |
krauss |
really fixed comment (cf. 7abeb749ae99)
|
file |
diff |
annotate
|
| Fri, 03 Dec 2010 08:40:47 +0100 |
bulwahn |
fixing comment in library
|
file |
diff |
annotate
|
| Sat, 27 Nov 2010 00:00:54 +0100 |
wenzelm |
merged;
|
file |
diff |
annotate
|
| Fri, 26 Nov 2010 23:13:58 +0100 |
haftmann |
strict forall2
|
file |
diff |
annotate
|
| Fri, 26 Nov 2010 22:29:41 +0100 |
wenzelm |
make two copies (!) of Library.UnequalLengths coincide with ListPair.UnequalLengths;
|
file |
diff |
annotate
|