Fri, 17 Jan 2025 16:03:35 +0100 minor performance tuning;
wenzelm [Fri, 17 Jan 2025 16:03:35 +0100] rev 81857
minor performance tuning;
Fri, 17 Jan 2025 15:39:40 +0100 clarified inst_type: more direct Thm.instantiate_frees;
wenzelm [Fri, 17 Jan 2025 15:39:40 +0100] rev 81856
clarified inst_type: more direct Thm.instantiate_frees;
Fri, 17 Jan 2025 14:47:25 +0100 more direct Thm.free: avoid re-certification;
wenzelm [Fri, 17 Jan 2025 14:47:25 +0100] rev 81855
more direct Thm.free: avoid re-certification;
Fri, 17 Jan 2025 14:31:48 +0100 clarified signature: more explicit types;
wenzelm [Fri, 17 Jan 2025 14:31:48 +0100] rev 81854
clarified signature: more explicit types;
Fri, 17 Jan 2025 13:44:45 +0100 tuned names;
wenzelm [Fri, 17 Jan 2025 13:44:45 +0100] rev 81853
tuned names;
Fri, 17 Jan 2025 13:04:34 +0100 tuned names;
wenzelm [Fri, 17 Jan 2025 13:04:34 +0100] rev 81852
tuned names;
Fri, 17 Jan 2025 13:00:39 +0100 tuned signature;
wenzelm [Fri, 17 Jan 2025 13:00:39 +0100] rev 81851
tuned signature;
(0) -30000 -10000 -3000 -1000 -300 -100 -30 -10 -7 +7 +10 +30 +100 +300 tip