src/Pure/General/history.ML
2007-06-13 wenzelm 2007-06-13 renamed map to map_current;
2006-11-04 wenzelm 2006-11-04 replaced apply_copy by apply'; tuned;
2005-06-20 wenzelm 2005-06-20 added previous;
2005-03-03 skalberg 2005-03-03 Move towards standard functions.
2005-02-13 skalberg 2005-02-13 Deleted Library.option type.
2004-06-21 kleing 2004-06-21 Merged in license change from Isabelle2004
2000-05-05 wenzelm 2000-05-05 GPLed;
1999-10-05 wenzelm 1999-10-05 clear: int arg;
1999-05-21 wenzelm 1999-05-21 optional limit; is_initial; apply_copy, map;
1998-06-16 wenzelm 1998-06-16 Histories of values, with undo and redo;