wenzelm [Tue, 21 Jan 2025 23:28:34 +0100] rev 81950
misc tuning;
wenzelm [Tue, 21 Jan 2025 23:17:21 +0100] rev 81949
tuned names;
wenzelm [Tue, 21 Jan 2025 23:15:03 +0100] rev 81948
more direct emulation of HOL Light inferences: prefer Pure rules over HOL thms;
represent hyps directly, using Thm.instantiate_frees followed by freeze' to ensure that no schematic vars remain (NB: Thm.generalize ignores type information);
use Thm.implies_elim / Thm.elim_implies directly, with proper exceptions instead of implicitly remaining hyps that cause trouble later;
def: proper freeze after retrieval of Isabelle thm;
wenzelm [Tue, 21 Jan 2025 19:49:13 +0100] rev 81947
tuned;
wenzelm [Tue, 21 Jan 2025 19:26:39 +0100] rev 81946
misc tuning: prefer specific variants of Thm.dest_comb;
wenzelm [Tue, 21 Jan 2025 19:26:09 +0100] rev 81945
more robust: explicit check for "Trueprop";
wenzelm [Tue, 21 Jan 2025 16:59:57 +0100] rev 81944
tuned;
wenzelm [Tue, 21 Jan 2025 16:50:46 +0100] rev 81943
more robust: explicit check for "Trueprop";
wenzelm [Tue, 21 Jan 2025 16:22:15 +0100] rev 81942
clarified signature: more uniform cterm operations, without context;
wenzelm [Tue, 21 Jan 2025 16:12:27 +0100] rev 81941
tuned;