Wed, 08 Jun 2011 16:20:18 +0200 |
don't generate unsound proof error for missing proofs
|
file | diff | annotate |
Tue, 07 Jun 2011 11:04:17 +0200 |
use the proper prover name, e.g. metis_full_types, not metis (full_types), for minimizing
|
file | diff | annotate |
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
|
file | diff | annotate |
Mon, 06 Jun 2011 20:56:06 +0200 |
Metis code cleanup
|
file | diff | annotate |
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"
|
file | diff | annotate |
Mon, 06 Jun 2011 20:36:35 +0200 |
imported patch metis_reconstr_give_type_infer_a_chance
|
file | diff | annotate |
Mon, 06 Jun 2011 20:36:35 +0200 |
make "metisX"'s default more like old "metis"
|
file | diff | annotate |
Mon, 06 Jun 2011 20:36:35 +0200 |
fixed reconstruction of new Skolem constants in new Metis
|
file | diff | annotate |
Mon, 06 Jun 2011 20:36:35 +0200 |
reveal Skolems in new Metis
|
file | diff | annotate |
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
|
file | diff | annotate |
Mon, 06 Jun 2011 20:36:35 +0200 |
slacker version of "fastype_of", in case a function has dummy type
|
file | diff | annotate |
Mon, 06 Jun 2011 20:36:35 +0200 |
only uncombine combinators in textual Isar proofs, not in Metis
|
file | diff | annotate |
Mon, 06 Jun 2011 20:36:34 +0200 |
temporarily added "MetisX" as reconstructor and minimizer
|
file | diff | annotate |
Mon, 06 Jun 2011 20:36:34 +0200 |
show what failed to play
|
file | diff | annotate |
Mon, 06 Jun 2011 20:36:34 +0200 |
killed odd connectives
|
file | diff | annotate |
Wed, 01 Jun 2011 10:29:43 +0200 |
handle lightweight tags sym theorems gracefully in the presence of TVars with interesting type classes
|
file | diff | annotate |
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
|
file | diff | annotate |
Wed, 01 Jun 2011 10:29:43 +0200 |
fixed interaction between type tags and hAPP in reconstruction code
|
file | diff | annotate |
Wed, 01 Jun 2011 10:29:43 +0200 |
implemented missing hAPP and ti cases of new path finder
|
file | diff | annotate |
Wed, 01 Jun 2011 10:29:43 +0200 |
export one more function
|
file | diff | annotate |
Tue, 31 May 2011 16:38:36 +0200 |
tuned name
|
file | diff | annotate |
Tue, 31 May 2011 16:38:36 +0200 |
more robust and simpler adjustment computation
|
file | diff | annotate |
Tue, 31 May 2011 16:38:36 +0200 |
more work on new Metis
|
file | diff | annotate |
Tue, 31 May 2011 16:38:36 +0200 |
tuning
|
file | diff | annotate |
Tue, 31 May 2011 16:38:36 +0200 |
first step in sharing more code between ATP and Metis translation
|
file | diff | annotate | base |