| #
dccdabe3 |
|
03-Mar-2016 |
wenzelm <none@none> |
clarified modules;
tuned signature;
|
| #
b32640c2 |
|
14-Dec-2015 |
wenzelm <none@none> |
tuned;
|
| #
e750bd28 |
|
11-May-2013 |
wenzelm <none@none> |
prefer explicitly qualified exceptions, which is particular important for robust handlers;
|
| #
3d5f7d6a |
|
10-Jan-2011 |
wenzelm <none@none> |
added merge_options convenience;
|
| #
ad727922 |
|
09-Sep-2010 |
wenzelm <none@none> |
more abstract treatment of interrupts in structure Exn -- hardly ever need to mention Interrupt literally;
|
| #
b6286729 |
|
06-Jun-2009 |
wenzelm <none@none> |
reraise exceptions to preserve position information;
|
| #
1bd59ac7 |
|
21-Jan-2009 |
wenzelm <none@none> |
removed Ids;
|
| #
7298aeec |
|
30-Sep-2008 |
wenzelm <none@none> |
more robust treatment of Interrupt (cf. exn.ML);
|
| #
bdf5119b |
|
03-Jul-2007 |
wenzelm <none@none> |
tuned;
|
| #
4d1c3488 |
|
12-Jun-2007 |
wenzelm <none@none> |
tuned;
|
| #
bc47772e |
|
03-Jun-2007 |
wenzelm <none@none> |
moved flip to library.ML;
removed unused dest/unfold/unfold_rev;
simplified fold/fold_rev/fold_map;
|
| #
9af63be6 |
|
11-May-2007 |
wenzelm <none@none> |
tuned;
|
| #
a1fe4da7 |
|
11-May-2007 |
krauss <none@none> |
added fun flip f x y = f y x
|
| #
2634fe7c |
|
15-Nov-2006 |
wenzelm <none@none> |
Fundamental concepts.
|