wenzelm [Wed, 21 Apr 2010 11:11:42 +0200] rev 36242
marked cygwin-poly as "e" test, which means further stages do not depend on it (website etc.);
huffman [Tue, 20 Apr 2010 13:44:28 -0700] rev 36241
replace many uses of Drule.export_without_context with Drule.zero_var_indexes
ballarin [Tue, 20 Apr 2010 22:34:17 +0200] rev 36240
Remove garbage.
ballarin [Tue, 20 Apr 2010 22:31:08 +0200] rev 36239
Remove garbage.
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
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 20 Apr 2010 14:55:53 +0200] rev 36214
eta-normalize the goal since the original theorem is atomized
wenzelm [Tue, 20 Apr 2010 11:31:14 +0200] rev 36213
accept x86_64 results gracefully -- NB: Mac OS does report that if booted in 64 bit mode;
wenzelm [Tue, 20 Apr 2010 11:26:25 +0200] rev 36212
refer to THIS_JAVA dynamically, and treat ISABELLE_JAVA as static default -- relevant for nested JVM invocation within an existing Isabelle enviroment;
haftmann [Tue, 20 Apr 2010 06:53:50 +0200] rev 36211
merged