| Tue, 21 Jan 2025 23:15:03 +0100 | wenzelm | more direct emulation of HOL Light inferences: prefer Pure rules over HOL thms; | changeset | files |
| Tue, 21 Jan 2025 19:49:13 +0100 | wenzelm | tuned; | changeset | files |
| Tue, 21 Jan 2025 19:26:39 +0100 | wenzelm | misc tuning: prefer specific variants of Thm.dest_comb; | changeset | files |
| Tue, 21 Jan 2025 19:26:09 +0100 | wenzelm | more robust: explicit check for "Trueprop"; | changeset | files |
| Tue, 21 Jan 2025 16:59:57 +0100 | wenzelm | tuned; | changeset | files |
| Tue, 21 Jan 2025 16:50:46 +0100 | wenzelm | more robust: explicit check for "Trueprop"; | changeset | files |
| Tue, 21 Jan 2025 16:22:15 +0100 | wenzelm | clarified signature: more uniform cterm operations, without context; | changeset | files |