summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files | gz |
help

(0) -30000 -10000 -3000 -1000 -300 -100 -10 +10 +100 +300 +1000 +3000 +10000 tip

(0) -30000 -10000 -3000 -1000 -300 -100 -10 +10 +100 +300 +1000 +3000 +10000 tip

don't forget the last inference(s) after conjecture skolemization

centralized & repaired handling of bound variables in intermediate data structure (viva de Bruijn)

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

renamed Sledgehammer options for symmetry between positive and negative versions

more robust w.r.t. exceptions raised by proof methods

tuning

compile

tuning

added 'algebra' and 'meson' to 'try0'

made 'try0' (more) silent