haftmann [Mon, 26 Apr 2010 15:37:50 +0200] rev 36409
use new classes (linordered_)field_inverse_zero
blanchet [Mon, 26 Apr 2010 23:46:45 +0200] rev 36408
merged
blanchet [Mon, 26 Apr 2010 23:45:51 +0200] rev 36407
renamed option
blanchet [Mon, 26 Apr 2010 23:45:32 +0200] rev 36406
fixes 2a5c6e7b55cb;
do not throw out the baby with the bath water
blanchet [Mon, 26 Apr 2010 21:50:36 +0200] rev 36405
compile
blanchet [Mon, 26 Apr 2010 21:41:54 +0200] rev 36404
make compile (and not just load dynamically)
blanchet [Mon, 26 Apr 2010 21:25:32 +0200] rev 36403
merge
blanchet [Mon, 26 Apr 2010 21:20:43 +0200] rev 36402
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
the code is still somewhat experimental but any exceptions it throws are catched, and Sledgehammer will still yield a one-line metis proof in case of proof reconstruction failure
blanchet [Mon, 26 Apr 2010 21:18:20 +0200] rev 36401
adapt code to reflect new signature of "neg_clausify"
blanchet [Mon, 26 Apr 2010 21:17:41 +0200] rev 36400
rename options and keep track of conjecture shape (to facilitate proof reconstruction)