| Sat, 18 Dec 2021 23:11:49 +0100 | desharna | tuned run_sledgehammer and called it directly from Mirabelle | changeset | files |
| Sat, 18 Dec 2021 14:30:13 +0100 | desharna | exported Sledgehammer.launch_prover and use it in Mirabelle | changeset | files |
| Sat, 18 Dec 2021 13:27:42 +0100 | desharna | proper filtering inf induction rules in Mirabelle | changeset | files |
| Fri, 17 Dec 2021 09:57:22 +0100 | desharna | added nearly_all_facts_of_context and uniformized its usage in Sledgehammer and Mirabelle | changeset | files |
| Fri, 17 Dec 2021 09:52:42 +0100 | desharna | tuned ATP to use is_widely_irrelevant_const | changeset | files |
| Fri, 17 Dec 2021 09:51:37 +0100 | desharna | added support for initialization messages to Mirabelle | changeset | files |
| Fri, 17 Dec 2021 16:36:42 +0100 | blanchet | tuned comment | changeset | files |