blanchet [Fri, 23 Apr 2010 12:24:30 +0200] rev 36294
compile
blanchet [Fri, 23 Apr 2010 12:07:12 +0200] rev 36293
handle SPASS's equality predicate correctly in Isar proof reconstruction
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