| Wed, 14 Jul 2021 16:09:57 +0200 | blanchet | prefer 'xxx' to 'xxx.yyy' to 'xxx(2)' in Sledgehammer, to some extent | changeset | files |
| Wed, 14 Jul 2021 15:18:11 +0200 | blanchet | tuning | changeset | files |
| Wed, 14 Jul 2021 14:24:55 +0200 | blanchet | rephrase Nitpick constraint in more first-order format that's also more friendly to the 'box' option | changeset | files |
| Wed, 14 Jul 2021 10:02:43 +0200 | blanchet | correctly translate constructor argument in 'primrec' | changeset | files |
| Tue, 13 Jul 2021 15:25:53 +0100 | paulson | simplified a few proofs | changeset | files |
| Tue, 13 Jul 2021 10:57:15 +0200 | blanchet | revisited ac28714b7478: more faithful preplaying with chained facts | changeset | files |
| Tue, 13 Jul 2021 10:57:14 +0200 | blanchet | wait for E 2.7 before using 'ite' in HO mode | changeset | files |