Mon, 14 Aug 2000 18:45:49 +0200 wenzelm tuned;
Mon, 14 Aug 2000 18:45:31 +0200 wenzelm updated;
Mon, 14 Aug 2000 18:45:16 +0200 wenzelm renamed 'intrs' to 'intros';
Mon, 14 Aug 2000 18:43:57 +0200 wenzelm updated command termination issue;
Mon, 14 Aug 2000 18:43:30 +0200 wenzelm some more refs;
Mon, 14 Aug 2000 18:42:57 +0200 wenzelm Aspinall:2000:eProof;
Mon, 14 Aug 2000 18:14:54 +0200 wenzelm raplaced "intrs" by "intrs" (new-style only);
(0) -3000 -1000 -300 -100 -30 -10 -7 +7 +10 +30 +100 +300 +1000 +3000 +10000 +30000 tip