84 - sledgehammer available_provers ~> sledgehammer supported_provers |
84 - sledgehammer available_provers ~> sledgehammer supported_provers |
85 INCOMPATIBILITY. |
85 INCOMPATIBILITY. |
86 - Added support for SNARK and ToFoF-E on SystemOnTPTP and for simply typed |
86 - Added support for SNARK and ToFoF-E on SystemOnTPTP and for simply typed |
87 TPTP problems (TFF). |
87 TPTP problems (TFF). |
88 - Added "type_sys", "max_mono_iters", and "max_new_mono_instances" options. |
88 - Added "type_sys", "max_mono_iters", and "max_new_mono_instances" options. |
|
89 - Removed "full_types" option and corresponding Proof General menu item. |
89 |
90 |
90 * Metis: |
91 * Metis: |
91 - Removed "metisF" -- use "metis" instead. |
92 - Removed "metisF" -- use "metis" instead. |
92 - Obsoleted "metisFT" -- use "metis (full_types)" instead. |
93 - Obsoleted "metisFT" -- use "metis (full_types)" instead. |
93 |
94 |
94 * "try": |
95 * "try": |
95 - Added "simp:", "intro:", and "elim:" options. |
96 - Renamed "try_methods" and added "simp:", "intro:", "dest:", and "elim:" |
|
97 options. INCOMPATIBILITY. |
|
98 - Introduced "try" that not only runs "try_methods" but also "solve_direct", |
|
99 "sledgehammer", "quickcheck", and "nitpick". |
96 |
100 |
97 * Quickcheck: |
101 * Quickcheck: |
98 - Added "eval" option to evaluate terms for the found counterexample |
102 - Added "eval" option to evaluate terms for the found counterexample |
99 (currently only supported by the default (exhaustive) tester) |
103 (currently only supported by the default (exhaustive) tester) |
100 - Added post-processing of terms to obtain readable counterexamples |
104 - Added post-processing of terms to obtain readable counterexamples |