| Thu, 30 Jan 2014 16:09:04 +0100 | haftmann | reduced prominence of "permissive code generation" | changeset | files |
| Thu, 30 Jan 2014 16:09:03 +0100 | haftmann | split rules for of_bool, similar to if | changeset | files |
| Thu, 30 Jan 2014 17:34:42 +0100 | blanchet | don't forget the last inference(s) after conjecture skolemization | changeset | files |
| Thu, 30 Jan 2014 16:40:31 +0100 | blanchet | centralized & repaired handling of bound variables in intermediate data structure (viva de Bruijn) | changeset | files |
| Thu, 30 Jan 2014 15:01:40 +0100 | blanchet | keep formula right before skolemization, because the universal variables might be different (or differently ordered) as in the original axiom or negated conjecture from which it was skolemized | changeset | files |
| Thu, 30 Jan 2014 14:37:53 +0100 | blanchet | renamed Sledgehammer options for symmetry between positive and negative versions | changeset | files |
| Thu, 30 Jan 2014 14:28:04 +0100 | blanchet | more robust w.r.t. exceptions raised by proof methods | changeset | files |