Sat, 05 Jul 2025 16:01:40 +0200 | wenzelm | minor performance tuning; | file | diff | annotate |
Sun, 09 Feb 2025 13:11:20 +0100 | wenzelm | tuned message; | file | diff | annotate |
Thu, 23 Jan 2025 20:46:26 +0100 | wenzelm | minor performance tuning: more fine-grained guard to skip irrelevant items; | file | diff | annotate |
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); | file | diff | annotate |
Wed, 22 Jan 2025 21:31:45 +0100 | wenzelm | tuned signature: more explicit operations; | file | diff | annotate |
Tue, 21 Jan 2025 15:48:39 +0100 | wenzelm | clarified exceptions; | file | diff | annotate |
Fri, 17 Jan 2025 14:47:25 +0100 | wenzelm | more direct Thm.free: avoid re-certification; | file | diff | annotate |