Mon, 06 Jun 2011 20:36:35 +0200 reveal Skolems in new Metis
blanchet [Mon, 06 Jun 2011 20:36:35 +0200] rev 43184
reveal Skolems in new Metis
Mon, 06 Jun 2011 20:36:35 +0200 don't throw exception on unknown constants (e.g. skolems), and give more precise type to applied functions
blanchet [Mon, 06 Jun 2011 20:36:35 +0200] rev 43183
don't throw exception on unknown constants (e.g. skolems), and give more precise type to applied functions
Mon, 06 Jun 2011 20:36:35 +0200 slacker version of "fastype_of", in case a function has dummy type
blanchet [Mon, 06 Jun 2011 20:36:35 +0200] rev 43182
slacker version of "fastype_of", in case a function has dummy type
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
(0) -30000 -10000 -3000 -1000 -300 -100 -10 +10 +100 +300 +1000 +3000 +10000 +30000 tip