Mon, 31 Jan 2022 16:09:23 +0100 | blanchet | updated documentation of 'slice' (now 'slices') option | changeset | files |
Mon, 31 Jan 2022 16:09:23 +0100 | blanchet | revised Sledgehammer documentation | changeset | files |
Mon, 31 Jan 2022 16:09:23 +0100 | blanchet | rationalized output for forthcoming slicing model | changeset | files |
Mon, 31 Jan 2022 16:09:23 +0100 | blanchet | use same default for FO and HO provers w.r.t. induction principles, based on evaluation -- this also simplifies the code | changeset | files |
Mon, 31 Jan 2022 16:09:23 +0100 | blanchet | disable slicing within ATP module (in preparation for refactoring) | changeset | files |
Mon, 31 Jan 2022 16:09:23 +0100 | blanchet | disable slicing within SMT (in preparation for factoring it out) | changeset | files |