2010-04-22 "remote_e" and "remote_vampire" support TSTP proof output + fix "overlord" mode ATP output postprocessing
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
2010-04-22 Isar proof reconstruction: type variables introduced by the ATP should be treated as type parameters for type inference purposes;
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
2010-04-22 postprocess ATP output in "overlord" mode to make it more readable
blanchet [Thu, 22 Apr 2010 10:13:02 +0200] rev 36284
postprocess ATP output in "overlord" mode to make it more readable
2010-04-21 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 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
2010-04-21 generate command-line in addition to timestamp in ATP output file, for debugging purposes
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
2010-04-21 pass relevant options from "sledgehammer" to "sledgehammer minimize";
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
2010-04-23 Finite set theory
Cezary Kaliszyk <kaliszyk@in.tum.de> [Fri, 23 Apr 2010 10:00:53 +0200] rev 36280
Finite set theory
(0) -30000 -10000 -3000 -1000 -300 -100 -30 -10 -7 +7 +10 +30 +100 +300 +1000 +3000 +10000 +30000 tip