blanchet [Mon, 19 Apr 2010 19:41:30 +0200] rev 36233
cosmetics
blanchet [Mon, 19 Apr 2010 19:41:15 +0200] rev 36232
don't redo an axiom selection in the first round of Sledgehammer "minimize"!;
this is needlessly slow and messes up the declared functions/predicates in SPASS DFG files
blanchet [Mon, 19 Apr 2010 18:44:12 +0200] rev 36231
get rid of "conjecture_pos", which is no longer necessary now that it's Metis's job, not Sledgehammer's, to report inconsistent contexts
blanchet [Mon, 19 Apr 2010 18:14:45 +0200] rev 36230
added warning about inconsistent context to Metis;
it makes more sense here than in Sledgehammer, because Sledgehammer is unsound and there's no point in having people panicking about the consistency of their context when their context is in fact consistent
blanchet [Mon, 19 Apr 2010 17:18:21 +0200] rev 36229
workaround for Proof General's off-by-a-few sendback display bug, whereby "pr" in "proof" is not highlighted
blanchet [Mon, 19 Apr 2010 16:33:48 +0200] rev 36228
got rid of somewhat pointless "pairname" function in Sledgehammer
blanchet [Mon, 19 Apr 2010 16:33:20 +0200] rev 36227
make Sledgehammer's "add:" and "del:" syntax really work (I hope), by comparing CNF theorems with CNF theorems
blanchet [Mon, 19 Apr 2010 16:29:52 +0200] rev 36226
cosmetics
blanchet [Mon, 19 Apr 2010 15:24:57 +0200] rev 36225
cosmetics
blanchet [Mon, 19 Apr 2010 15:21:35 +0200] rev 36224
cosmetics