blanchet [Thu, 30 Jan 2014 17:34:42 +0100] rev 55186
don't forget the last inference(s) after conjecture skolemization
blanchet [Thu, 30 Jan 2014 16:40:31 +0100] rev 55185
centralized & repaired handling of bound variables in intermediate data structure (viva de Bruijn)
blanchet [Thu, 30 Jan 2014 15:01:40 +0100] rev 55184
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
blanchet [Thu, 30 Jan 2014 14:37:53 +0100] rev 55183
renamed Sledgehammer options for symmetry between positive and negative versions
blanchet [Thu, 30 Jan 2014 14:28:04 +0100] rev 55182
more robust w.r.t. exceptions raised by proof methods
blanchet [Thu, 30 Jan 2014 14:24:10 +0100] rev 55181
tuning
blanchet [Thu, 30 Jan 2014 13:54:12 +0100] rev 55180
compile
blanchet [Thu, 30 Jan 2014 13:39:57 +0100] rev 55179
tuning
blanchet [Thu, 30 Jan 2014 13:38:28 +0100] rev 55178
added 'algebra' and 'meson' to 'try0'
blanchet [Thu, 30 Jan 2014 13:38:28 +0100] rev 55177
made 'try0' (more) silent