| Wed, 19 Apr 2023 14:48:43 +0200 | wenzelm | minor performance tuning: recursive check of pointer_eq; | changeset | files |
| Wed, 19 Apr 2023 14:29:52 +0200 | wenzelm | minor performance tuning: avoid excessive (de)constructions for base cases; | changeset | files |
| Wed, 19 Apr 2023 11:10:52 +0200 | wenzelm | unused (see also 864c7c684651 and b6aa5eac0a1a); | changeset | files |
| Wed, 19 Apr 2023 11:10:30 +0200 | wenzelm | tuned; | changeset | files |
| Tue, 18 Apr 2023 22:24:48 +0200 | wenzelm | tuned; | changeset | files |
| Tue, 18 Apr 2023 21:47:40 +0200 | wenzelm | more operations: avoid intermediate list; | changeset | files |
| Tue, 18 Apr 2023 21:03:24 +0200 | wenzelm | discontinued somewhat pointless operation: Conjunction.intr_balanced / Conjunction.elim_balanced with single hyp performs better (e.g. see AFP/351b7b576892); | changeset | files |