blanchet [Thu, 22 Apr 2010 14:47:52 +0200] rev 36287
if Isar proof reconstruction is not supported, tell the user so they don't wonder why their "isar_proof" option did nothing
blanchet [Thu, 22 Apr 2010 13:50:58 +0200] rev 36286
"remote_e" and "remote_vampire" support TSTP proof output + fix "overlord" mode ATP output postprocessing
blanchet [Thu, 22 Apr 2010 10:54:56 +0200] rev 36285
Isar proof reconstruction: type variables introduced by the ATP should be treated as type parameters for type inference purposes;
this solves the unification exception that consistently was thrown for Cezary's "FSet3" theory
blanchet [Thu, 22 Apr 2010 10:13:02 +0200] rev 36284
postprocess ATP output in "overlord" mode to make it more readable
blanchet [Wed, 21 Apr 2010 17:06:26 +0200] rev 36283
failure of reconstructing the Isar proof (e.g., exception) should not prevent Sledgehammer from showing the short one-liner proof -- but in "debug" mode we do want to know what the exception is
blanchet [Wed, 21 Apr 2010 16:38:03 +0200] rev 36282
generate command-line in addition to timestamp in ATP output file, for debugging purposes
blanchet [Wed, 21 Apr 2010 16:21:19 +0200] rev 36281
pass relevant options from "sledgehammer" to "sledgehammer minimize";
one nice side effect of this change is that the "sledgehammer minimize" syntax now only occurs in "sledgehammer_isar.ML", instead of being spread across two files