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)
blanchet [Mon, 26 Apr 2010 21:17:04 +0200] rev 36399
rename options
blanchet [Mon, 26 Apr 2010 21:16:35 +0200] rev 36398
make "neg_clausify" return a list of lists of clauses, so that it's possible to see which clause comes from which theorem
blanchet [Mon, 26 Apr 2010 21:14:28 +0200] rev 36397
remove needless code that was copy-pasted from Quickcheck (where it made sense)
blanchet [Sun, 25 Apr 2010 15:30:33 +0200] rev 36396
cosmetics
blanchet [Sun, 25 Apr 2010 15:04:20 +0200] rev 36395
cosmetics
blanchet [Sun, 25 Apr 2010 14:40:36 +0200] rev 36394
move "neg_clausify" method and "clausify" attribute to "sledgehammer_isar.ML"