src/HOL/Tools/ATP/atp_translate.ML
Mon, 06 Jun 2011 20:36:35 +0200 blanchet tuning
Mon, 06 Jun 2011 20:36:35 +0200 blanchet fixed detection of Skolem constants in type construction detection code
Mon, 06 Jun 2011 20:36:35 +0200 blanchet also exploit type tag idempotence in lightweight encodings, following a suggestion from Gothenburg
Mon, 06 Jun 2011 20:36:35 +0200 blanchet don't stumble on Skolem names
Mon, 06 Jun 2011 20:36:35 +0200 blanchet 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 blanchet 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 blanchet properly locate helpers whose constants have several entries in the helper table
Mon, 06 Jun 2011 20:36:35 +0200 blanchet skip "hBOOL" in new Metis path finder
Mon, 06 Jun 2011 20:36:34 +0200 blanchet ensured that the logic for "explicit_apply = smart" also works on CNF (i.e. new Metis)
Mon, 06 Jun 2011 20:36:34 +0200 blanchet added support for helpers in new Metis, so far only for polymorphic type encodings
Wed, 01 Jun 2011 19:50:59 +0200 blanchet fixed debilitating translation bug introduced in b6e61d22fa61 -- "equal" and "=" should always have arity 2
Wed, 01 Jun 2011 10:29:43 +0200 blanchet handle lightweight tags sym theorems gracefully in the presence of TVars with interesting type classes
Wed, 01 Jun 2011 10:29:43 +0200 blanchet implemented missing hAPP and ti cases of new path finder
Wed, 01 Jun 2011 10:29:43 +0200 blanchet support lightweight tags in new Metis
Wed, 01 Jun 2011 10:29:43 +0200 blanchet tuned names
Wed, 01 Jun 2011 10:29:43 +0200 blanchet distinguish different kinds of typing informations in the fact name
Wed, 01 Jun 2011 00:23:16 +0200 blanchet make SML/NJ happier
Wed, 01 Jun 2011 00:12:38 +0200 blanchet make sure "Trueprop" is removed before combinators are added -- the code is fragile in that respect
Tue, 31 May 2011 16:38:36 +0200 blanchet no need for type arguments with "xxx_tags_heavy" type system
Tue, 31 May 2011 16:38:36 +0200 blanchet use ":" for type information (looks good in Metis's output) and handle it in new path finder
Tue, 31 May 2011 16:38:36 +0200 blanchet tuned name
Tue, 31 May 2011 16:38:36 +0200 blanchet make "prepare_atp_problem" more robust w.r.t. choice of type system
Tue, 31 May 2011 16:38:36 +0200 blanchet proper handling of type variable classes in new Metis
Tue, 31 May 2011 16:38:36 +0200 blanchet don't preprocess twice
Tue, 31 May 2011 16:38:36 +0200 blanchet tuning
Tue, 31 May 2011 16:38:36 +0200 blanchet more work on new metis that exploits the powerful new type encodings
Tue, 31 May 2011 16:38:36 +0200 blanchet tuning
Tue, 31 May 2011 16:38:36 +0200 blanchet first step in sharing more code between ATP and Metis translation
less more (0) tip