src/Pure/General/history.ML
Wed, 13 Jun 2007 00:02:02 +0200 wenzelm renamed map to map_current;
Sat, 04 Nov 2006 19:25:41 +0100 wenzelm replaced apply_copy by apply';
Mon, 20 Jun 2005 22:14:10 +0200 wenzelm added previous;
Thu, 03 Mar 2005 12:43:01 +0100 skalberg Move towards standard functions.
Sun, 13 Feb 2005 17:15:14 +0100 skalberg Deleted Library.option type.
Mon, 21 Jun 2004 10:25:57 +0200 kleing Merged in license change from Isabelle2004
Fri, 05 May 2000 22:02:46 +0200 wenzelm GPLed;
Tue, 05 Oct 1999 15:28:37 +0200 wenzelm clear: int arg;
Fri, 21 May 1999 11:36:56 +0200 wenzelm optional limit;
Tue, 16 Jun 1998 18:37:11 +0200 wenzelm Histories of values, with undo and redo;
less more (0) tip