src/Pure/thm.ML
Sat, 05 Jul 2025 16:01:40 +0200 wenzelm minor performance tuning;
Sun, 09 Feb 2025 13:11:20 +0100 wenzelm tuned message;
Thu, 23 Jan 2025 20:46:26 +0100 wenzelm minor performance tuning: more fine-grained guard to skip irrelevant items;
Thu, 23 Jan 2025 20:06:14 +0100 wenzelm proper treatment of variables with the same name, but different sorts/types: this routinely happens in HOL Light (see also 0e2f019477e2), as well as theory "HOL-Algebra.Algebraic_Closure_Type" (line 77);
Wed, 22 Jan 2025 21:31:45 +0100 wenzelm tuned signature: more explicit operations;
Tue, 21 Jan 2025 15:48:39 +0100 wenzelm clarified exceptions;
Fri, 17 Jan 2025 14:47:25 +0100 wenzelm more direct Thm.free: avoid re-certification;
less more (0) -300 -100 -30 -10 -7 tip