Mon, 15 May 2023 20:19:02 +0200 tuned signature;
wenzelm [Mon, 15 May 2023 20:19:02 +0200] rev 78057
tuned signature;
Mon, 15 May 2023 19:40:01 +0200 more accurate Thm.trim_context / Thm.transfer;
wenzelm [Mon, 15 May 2023 19:40:01 +0200] rev 78056
more accurate Thm.trim_context / Thm.transfer;
Mon, 15 May 2023 16:18:23 +0200 clarified stored thm: result from notes;
wenzelm [Mon, 15 May 2023 16:18:23 +0200] rev 78055
clarified stored thm: result from notes; tuned;
Mon, 15 May 2023 15:14:19 +0200 tuned whitespace;
wenzelm [Mon, 15 May 2023 15:14:19 +0200] rev 78054
tuned whitespace;
Mon, 15 May 2023 15:04:37 +0200 clarified signature: avoid convoluted operations;
wenzelm [Mon, 15 May 2023 15:04:37 +0200] rev 78053
clarified signature: avoid convoluted operations;
Mon, 15 May 2023 14:34:38 +0200 tuned signature;
wenzelm [Mon, 15 May 2023 14:34:38 +0200] rev 78052
tuned signature;
Mon, 15 May 2023 14:21:00 +0200 update to polyml-a5d5fba90286, with more robust ML_Heap.sizeof;
wenzelm [Mon, 15 May 2023 14:21:00 +0200] rev 78051
update to polyml-a5d5fba90286, with more robust ML_Heap.sizeof;
(0) -30000 -10000 -3000 -1000 -300 -100 -30 -10 -7 +7 +10 +30 +100 +300 +1000 tip