src/HOL/Tools/ATP/atp_reconstruct.ML
Wed, 08 Jun 2011 16:20:18 +0200 don't generate unsound proof error for missing proofs
Tue, 07 Jun 2011 11:04:17 +0200 use the proper prover name, e.g. metis_full_types, not metis (full_types), for minimizing
Tue, 07 Jun 2011 08:52:35 +0200 obsoleted "metisFT", and added "no_types" version of Metis as fallback to Sledgehammer after noticing how useful it can be
Mon, 06 Jun 2011 20:56:06 +0200 Metis code cleanup
Mon, 06 Jun 2011 20:36:35 +0200 remove more occurrences of "metisX", preparing for the D Day when it will silently hijack "metis" and "metisFT"
Mon, 06 Jun 2011 20:36:35 +0200 imported patch metis_reconstr_give_type_infer_a_chance
Mon, 06 Jun 2011 20:36:35 +0200 make "metisX"'s default more like old "metis"
Mon, 06 Jun 2011 20:36:35 +0200 fixed reconstruction of new Skolem constants in new Metis
Mon, 06 Jun 2011 20:36:35 +0200 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
Mon, 06 Jun 2011 20:36:35 +0200 slacker version of "fastype_of", in case a function has dummy type
Mon, 06 Jun 2011 20:36:35 +0200 only uncombine combinators in textual Isar proofs, not in Metis
Mon, 06 Jun 2011 20:36:34 +0200 temporarily added "MetisX" as reconstructor and minimizer
Mon, 06 Jun 2011 20:36:34 +0200 show what failed to play
Mon, 06 Jun 2011 20:36:34 +0200 killed odd connectives
Wed, 01 Jun 2011 10:29:43 +0200 handle lightweight tags sym theorems gracefully in the presence of TVars with interesting type classes
Wed, 01 Jun 2011 10:29:43 +0200 more uniform handling of tfree sort inference in ATP reconstruction code, based on what Metis always has done
Wed, 01 Jun 2011 10:29:43 +0200 fixed interaction between type tags and hAPP in reconstruction code
Wed, 01 Jun 2011 10:29:43 +0200 implemented missing hAPP and ti cases of new path finder
Wed, 01 Jun 2011 10:29:43 +0200 export one more function
Tue, 31 May 2011 16:38:36 +0200 tuned name
Tue, 31 May 2011 16:38:36 +0200 more robust and simpler adjustment computation
Tue, 31 May 2011 16:38:36 +0200 more work on new Metis
Tue, 31 May 2011 16:38:36 +0200 tuning
Tue, 31 May 2011 16:38:36 +0200 first step in sharing more code between ATP and Metis translation