blanchet [Fri, 23 Apr 2010 11:34:49 +0200] rev 36292
merged
blanchet [Fri, 23 Apr 2010 11:32:36 +0200] rev 36291
added Isar proof reconstruction support for SPASS -- which means all provers can now yield Isar proofs;
the implementation might still be flaky, but exceptions are caught so that a proof reconstruction failure doesn't result in a Sledgehammer failure (the one-line Metis proof might still work after all)
blanchet [Thu, 22 Apr 2010 16:30:54 +0200] rev 36290
remove hack that is no longer necessary now that "ATP_Wrapper" properly detects which ATPs are installed
blanchet [Thu, 22 Apr 2010 16:30:04 +0200] rev 36289
set "atps" reference's default value to "(remote_)e (remote_)spass (remote_)vampire", based on what is installed
blanchet [Thu, 22 Apr 2010 15:01:36 +0200] rev 36288
minor code cleanup
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