| Sun, 24 Dec 2023 11:13:33 +0100 |
wenzelm |
more operations;
|
file |
diff |
annotate
|
| Tue, 16 May 2023 14:30:32 +0200 |
wenzelm |
support for context within morphism (for background theory);
|
file |
diff |
annotate
|
| Thu, 03 Mar 2016 15:23:02 +0100 |
wenzelm |
clarified modules;
|
file |
diff |
annotate
|
| Mon, 14 Dec 2015 11:47:32 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Sat, 11 May 2013 16:57:18 +0200 |
wenzelm |
prefer explicitly qualified exceptions, which is particular important for robust handlers;
|
file |
diff |
annotate
|
| Mon, 10 Jan 2011 16:45:28 +0100 |
wenzelm |
added merge_options convenience;
|
file |
diff |
annotate
|
| Thu, 09 Sep 2010 17:20:27 +0200 |
wenzelm |
more abstract treatment of interrupts in structure Exn -- hardly ever need to mention Interrupt literally;
|
file |
diff |
annotate
|
| Sat, 06 Jun 2009 21:47:02 +0200 |
wenzelm |
reraise exceptions to preserve position information;
|
file |
diff |
annotate
|
| Wed, 21 Jan 2009 23:21:44 +0100 |
wenzelm |
removed Ids;
|
file |
diff |
annotate
|
| Wed, 01 Oct 2008 12:00:02 +0200 |
wenzelm |
more robust treatment of Interrupt (cf. exn.ML);
|
file |
diff |
annotate
|
| Tue, 03 Jul 2007 22:27:25 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Wed, 13 Jun 2007 00:02:01 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Sun, 03 Jun 2007 23:16:53 +0200 |
wenzelm |
moved flip to library.ML;
|
file |
diff |
annotate
|
| Fri, 11 May 2007 17:54:36 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Fri, 11 May 2007 15:37:42 +0200 |
krauss |
added fun flip f x y = f y x
|
file |
diff |
annotate
|