wenzelm [Tue, 20 Apr 2010 17:07:53 +0200] rev 36238
recovered isabelle java, which was broken in ebfa4bb0d50f;
blanchet [Tue, 20 Apr 2010 16:14:45 +0200] rev 36237
fix bug in SPASS's DFG output files, where "tc_bool" wasn't declared;
this bug occurs when the explicit "hAPP" or "hBOOL" functions are introduced and full types is activated
blanchet [Tue, 20 Apr 2010 16:04:49 +0200] rev 36236
merged
blanchet [Tue, 20 Apr 2010 16:04:36 +0200] rev 36235
added "explicit_apply" option to Sledgehammer, to control whether an explicit apply function should be used as much or as little as possible (replaces a previous global variable)
blanchet [Tue, 20 Apr 2010 14:39:42 +0200] rev 36234
merge
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