Mon, 18 Dec 2023 22:49:33 +0100 more thorough beta contraction;
wenzelm [Mon, 18 Dec 2023 22:49:33 +0100] rev 79286
more thorough beta contraction; removed unused operations;
Mon, 18 Dec 2023 22:11:13 +0100 tuned whitespace;
wenzelm [Mon, 18 Dec 2023 22:11:13 +0100] rev 79285
tuned whitespace;
Mon, 18 Dec 2023 21:52:55 +0100 tuned;
wenzelm [Mon, 18 Dec 2023 21:52:55 +0100] rev 79284
tuned;
(0) -30000 -10000 -3000 -1000 -300 -100 -30 -10 -3 +3 +10 +30 +100 +300 +1000 tip