src/Pure/General/basics.ML
Mon, 14 Dec 2015 11:47:32 +0100 wenzelm tuned;
Sat, 11 May 2013 16:57:18 +0200 wenzelm prefer explicitly qualified exceptions, which is particular important for robust handlers;
Mon, 10 Jan 2011 16:45:28 +0100 wenzelm added merge_options convenience;
Thu, 09 Sep 2010 17:20:27 +0200 wenzelm more abstract treatment of interrupts in structure Exn -- hardly ever need to mention Interrupt literally;
Sat, 06 Jun 2009 21:47:02 +0200 wenzelm reraise exceptions to preserve position information;
Wed, 21 Jan 2009 23:21:44 +0100 wenzelm removed Ids;
Wed, 01 Oct 2008 12:00:02 +0200 wenzelm more robust treatment of Interrupt (cf. exn.ML);
Tue, 03 Jul 2007 22:27:25 +0200 wenzelm tuned;
Wed, 13 Jun 2007 00:02:01 +0200 wenzelm tuned;
Sun, 03 Jun 2007 23:16:53 +0200 wenzelm moved flip to library.ML;
Fri, 11 May 2007 17:54:36 +0200 wenzelm tuned;
Fri, 11 May 2007 15:37:42 +0200 krauss added fun flip f x y = f y x
Thu, 16 Nov 2006 01:07:23 +0100 wenzelm Fundamental concepts.
less more (0) tip