wenzelm [Mon, 11 Dec 2023 21:56:24 +0100] rev 79255
merged
wenzelm [Mon, 11 Dec 2023 21:31:58 +0100] rev 79254
minor performance tuning;
wenzelm [Mon, 11 Dec 2023 21:17:28 +0100] rev 79253
tuned;
wenzelm [Mon, 11 Dec 2023 21:09:24 +0100] rev 79252
minor performance tuning: prefer Same.operation;
wenzelm [Mon, 11 Dec 2023 20:53:01 +0100] rev 79251
clarified signature;
minor performance tuning: avoid redundant identity;
wenzelm [Mon, 11 Dec 2023 20:17:13 +0100] rev 79250
minor performance tuning;
wenzelm [Mon, 11 Dec 2023 19:51:30 +0100] rev 79249
more operations;
wenzelm [Mon, 11 Dec 2023 19:36:28 +0100] rev 79248
revert 17fda85a33dc: renaming is not necessarily unique, e.g. [("x", "x"), ("x", "y")];
wenzelm [Mon, 11 Dec 2023 19:33:31 +0100] rev 79247
misc tuning and clarification;
wenzelm [Mon, 11 Dec 2023 14:26:24 +0100] rev 79246
minor performance tuning: prefer Symset.T;
tuned names;