src/Pure/General/history.ML
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