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