Fri, 07 Jun 2024 13:46:51 +0200 tuned: prefer Thm_Name operations;
wenzelm [Fri, 07 Jun 2024 13:46:51 +0200] rev 80292
tuned: prefer Thm_Name operations;
Fri, 07 Jun 2024 13:40:12 +0200 tuned;
wenzelm [Fri, 07 Jun 2024 13:40:12 +0200] rev 80291
tuned;
(0) -30000 -10000 -3000 -1000 -300 -100 -30 -10 -2 +2 +10 +30 +100 +300 +1000 tip