src/Pure/General/history.ML
Tue, 16 Jun 1998 18:37:11 +0200 wenzelm Histories of values, with undo and redo;
less more (0) tip