Sat, 07 Dec 2024 23:50:18 +0100 clarified term positions and markup: syntax = true means this is via concrete syntax;
wenzelm [Sat, 07 Dec 2024 23:50:18 +0100] rev 81558
clarified term positions and markup: syntax = true means this is via concrete syntax; clarified text color rendering;
Sat, 07 Dec 2024 23:08:51 +0100 tuned signature: more operations;
wenzelm [Sat, 07 Dec 2024 23:08:51 +0100] rev 81557
tuned signature: more operations;
Sat, 07 Dec 2024 21:49:05 +0100 tuned;
wenzelm [Sat, 07 Dec 2024 21:49:05 +0100] rev 81556
tuned;
Sat, 07 Dec 2024 21:42:59 +0100 clarified signature: more explicit operations;
wenzelm [Sat, 07 Dec 2024 21:42:59 +0100] rev 81555
clarified signature: more explicit operations;
Sat, 07 Dec 2024 16:07:48 +0100 tuned;
wenzelm [Sat, 07 Dec 2024 16:07:48 +0100] rev 81554
tuned;
Sat, 07 Dec 2024 16:03:05 +0100 tuned whitespace;
wenzelm [Sat, 07 Dec 2024 16:03:05 +0100] rev 81553
tuned whitespace;
(0) -30000 -10000 -3000 -1000 -300 -100 -30 -10 -6 +6 +10 +30 +100 +300 +1000 tip