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
Mon, 06 Jun 2011 20:36:35 +0200 gracefully handle the case where a constant is partially or not instantiated at all, as may happen when reconstructing Metis proofs for polymorphic type encodings
blanchet [Mon, 06 Jun 2011 20:36:35 +0200] rev 43171
gracefully handle the case where a constant is partially or not instantiated at all, as may happen when reconstructing Metis proofs for polymorphic type encodings
Mon, 06 Jun 2011 20:36:35 +0200 temporarily document "metisX"
blanchet [Mon, 06 Jun 2011 20:36:35 +0200] rev 43170
temporarily document "metisX"
(0) -30000 -10000 -3000 -1000 -300 -100 -10 +10 +100 +300 +1000 +3000 +10000 tip