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
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
blanchet [Mon, 19 Apr 2010 15:15:21 +0200] rev 36223
make Sledgehammer's minimizer also minimize Isar proofs
blanchet [Mon, 19 Apr 2010 11:54:07 +0200] rev 36222
don't use readable names if proof reconstruction is needed, because it uses the structure of names
blanchet [Mon, 19 Apr 2010 11:02:00 +0200] rev 36221
allow "_" in TPTP names in debug mode
blanchet [Mon, 19 Apr 2010 10:45:08 +0200] rev 36220
rename Sledgehammer "theory_const" option to "theory_relevant", now that I understand better what it does
blanchet [Mon, 19 Apr 2010 10:15:02 +0200] rev 36219
set SPASS option on the command-line, so that it doesn't vanish when moving to TPTP format
blanchet [Mon, 19 Apr 2010 09:53:31 +0200] rev 36218
get rid of "List.foldl" + add timestamp to SPASS
wenzelm [Tue, 20 Apr 2010 15:17:18 +0200] rev 36217
less ambitious settings for cygwin-poly;
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 20 Apr 2010 14:56:58 +0200] rev 36216
respectfullness and preservation of map for identity quotients
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 20 Apr 2010 14:56:20 +0200] rev 36215
respectfullness and preservation of function composition