Mon, 06 Jun 2011 20:36:35 +0200 don't stumble on Skolem names
blanchet [Mon, 06 Jun 2011 20:36:35 +0200] rev 43181
don't stumble on Skolem names
Mon, 06 Jun 2011 20:36:35 +0200 conceal old Skolems in new Metis
blanchet [Mon, 06 Jun 2011 20:36:35 +0200] rev 43180
conceal old Skolems in new Metis
Mon, 06 Jun 2011 20:36:35 +0200 don't merge "hAPP"s even in unsound heavy modes, because "hAPP" then sometimes gets declared with too strict arguments ("ind"), and we lose some proofs
blanchet [Mon, 06 Jun 2011 20:36:35 +0200] rev 43179
don't merge "hAPP"s even in unsound heavy modes, because "hAPP" then sometimes gets declared with too strict arguments ("ind"), and we lose some proofs
Mon, 06 Jun 2011 20:36:35 +0200 use "" type only in THF and TFF -- might cause strange failures if used in FOF or CNF, depending on how liberal the prover is
blanchet [Mon, 06 Jun 2011 20:36:35 +0200] rev 43178
use "" type only in THF and TFF -- might cause strange failures if used in FOF or CNF, depending on how liberal the prover is
Mon, 06 Jun 2011 20:36:35 +0200 properly unmangle names in path finder
blanchet [Mon, 06 Jun 2011 20:36:35 +0200] rev 43177
properly unmangle names in path finder
Mon, 06 Jun 2011 20:36:35 +0200 only uncombine combinators in textual Isar proofs, not in Metis
blanchet [Mon, 06 Jun 2011 20:36:35 +0200] rev 43176
only uncombine combinators in textual Isar proofs, not in Metis
Mon, 06 Jun 2011 20:36:35 +0200 properly locate helpers whose constants have several entries in the helper table
blanchet [Mon, 06 Jun 2011 20:36:35 +0200] rev 43175
properly locate helpers whose constants have several entries in the helper table
Mon, 06 Jun 2011 20:36:35 +0200 skip "hBOOL" in new Metis path finder
blanchet [Mon, 06 Jun 2011 20:36:35 +0200] rev 43174
skip "hBOOL" in new Metis path finder
Mon, 06 Jun 2011 20:36:35 +0200 don't pass "~ " to new Metis
blanchet [Mon, 06 Jun 2011 20:36:35 +0200] rev 43173
don't pass "~ " to new Metis
Mon, 06 Jun 2011 20:36:35 +0200 tuning
blanchet [Mon, 06 Jun 2011 20:36:35 +0200] rev 43172
tuning
(0) -30000 -10000 -3000 -1000 -300 -100 -10 +10 +100 +300 +1000 +3000 +10000 +30000 tip