blanchet [Tue, 07 Jun 2011 08:52:35 +0200] rev 43228
obsoleted "metisFT", and added "no_types" version of Metis as fallback to Sledgehammer after noticing how useful it can be
blanchet [Tue, 07 Jun 2011 07:57:24 +0200] rev 43227
fixed typo in legacy feature message
blanchet [Tue, 07 Jun 2011 07:45:12 +0200] rev 43226
use new monomorphization code
blanchet [Tue, 07 Jun 2011 07:44:54 +0200] rev 43225
added (currently unused) verbose configuration option
blanchet [Tue, 07 Jun 2011 07:06:24 +0200] rev 43224
renamed ML function
blanchet [Tue, 07 Jun 2011 07:04:53 +0200] rev 43223
renamed example theory to "ATP_Export", for consistency with its underlying "ATP_" modules
blanchet [Tue, 07 Jun 2011 06:58:52 +0200] rev 43222
pass props not thms to ATP translator
blanchet [Mon, 06 Jun 2011 23:46:02 +0200] rev 43221
slighly more reasonable Vampire slices (until new monomorphizer is used)
blanchet [Mon, 06 Jun 2011 23:43:28 +0200] rev 43220
removed confusing slicing logic
blanchet [Mon, 06 Jun 2011 23:26:40 +0200] rev 43219
suggest first reconstructor that timed out, not last (i.e. metis not metisFT in most cases)
blanchet [Mon, 06 Jun 2011 23:11:14 +0200] rev 43218
effectively reenable slices for SPASS and Vampire -- they were disabled by mistake
blanchet [Mon, 06 Jun 2011 22:03:58 +0200] rev 43217
minor: curly brackets, not square brackets
blanchet [Mon, 06 Jun 2011 21:58:29 +0200] rev 43216
document metis better in Sledgehammer docs
blanchet [Mon, 06 Jun 2011 21:02:24 +0200] rev 43215
updated Sledgehammer message
blanchet [Mon, 06 Jun 2011 20:56:06 +0200] rev 43214
removed old optimization that isn't one anyone
blanchet [Mon, 06 Jun 2011 20:56:06 +0200] rev 43213
generate less type information in polymorphic case
blanchet [Mon, 06 Jun 2011 20:56:06 +0200] rev 43212
Metis code cleanup
blanchet [Mon, 06 Jun 2011 20:36:36 +0200] rev 43211
enable new Metis
blanchet [Mon, 06 Jun 2011 20:36:35 +0200] rev 43210
made "explicit_apply"'s smart mode (more) complete
blanchet [Mon, 06 Jun 2011 20:36:35 +0200] rev 43209
fall back in case path finder fails -- these errors are sometimes salvageable
blanchet [Mon, 06 Jun 2011 20:36:35 +0200] rev 43208
compile
blanchet [Mon, 06 Jun 2011 20:36:35 +0200] rev 43207
change var name as a workaround for rare issue in Metis's reconstruction code -- namely, "find_var" fails because "X = X" is wrongly mirrorred as "A = A"
blanchet [Mon, 06 Jun 2011 20:36:35 +0200] rev 43206
marked "metisF" as legacy -- nobody uses it or needs it
blanchet [Mon, 06 Jun 2011 20:36:35 +0200] rev 43205
more preparations towards hijacking Metis
blanchet [Mon, 06 Jun 2011 20:36:35 +0200] rev 43204
remove more occurrences of "metisX", preparing for the D Day when it will silently hijack "metis" and "metisFT"
blanchet [Mon, 06 Jun 2011 20:36:35 +0200] rev 43203
don't mention "metisX" so much in the docs -- it will go away soon
blanchet [Mon, 06 Jun 2011 20:36:35 +0200] rev 43202
reintroduced metisFT in example
blanchet [Mon, 06 Jun 2011 20:36:35 +0200] rev 43201
make "smart" mode of "explicit_apply" smarter, by also detecting the other kind of higher-order quantification, namely "bool"s
blanchet [Mon, 06 Jun 2011 20:36:35 +0200] rev 43200
imported patch metis_reconstr_give_type_infer_a_chance
blanchet [Mon, 06 Jun 2011 20:36:35 +0200] rev 43199
make "metisX"'s default more like old "metis"
blanchet [Mon, 06 Jun 2011 20:36:35 +0200] rev 43198
whitespace tuning
blanchet [Mon, 06 Jun 2011 20:36:35 +0200] rev 43197
tuned Metis examples
blanchet [Mon, 06 Jun 2011 20:36:35 +0200] rev 43196
more through tests of new Metis
blanchet [Mon, 06 Jun 2011 20:36:35 +0200] rev 43195
improved correctness of handling of higher-order occurrences of "Not" in new Metis (and probably in old Metis)
blanchet [Mon, 06 Jun 2011 20:36:35 +0200] rev 43194
fixed type helper indices in new Metis
blanchet [Mon, 06 Jun 2011 20:36:35 +0200] rev 43193
improved ATP clausifier so it can deal with "x => (y <=> z)"
blanchet [Mon, 06 Jun 2011 20:36:35 +0200] rev 43192
avoid renumbering hypotheses
blanchet [Mon, 06 Jun 2011 20:36:35 +0200] rev 43191
fixed reconstruction of new Skolem constants in new Metis
blanchet [Mon, 06 Jun 2011 20:36:35 +0200] rev 43190
don't translate new Skolemizer assumptions in new Metis
blanchet [Mon, 06 Jun 2011 20:36:35 +0200] rev 43189
tuning
blanchet [Mon, 06 Jun 2011 20:36:35 +0200] rev 43188
fixed detection of Skolem constants in type construction detection code
blanchet [Mon, 06 Jun 2011 20:36:35 +0200] rev 43187
make resolution replay more robust, in case Metis distinguishes between two literals that are merged in Isabelle (e.g. because they carry more or less type annotations in Metis)
blanchet [Mon, 06 Jun 2011 20:36:35 +0200] rev 43186
tuning
blanchet [Mon, 06 Jun 2011 20:36:35 +0200] rev 43185
also exploit type tag idempotence in lightweight encodings, following a suggestion from Gothenburg
blanchet [Mon, 06 Jun 2011 20:36:35 +0200] rev 43184
reveal Skolems in new Metis
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
blanchet [Mon, 06 Jun 2011 20:36:35 +0200] rev 43182
slacker version of "fastype_of", in case a function has dummy type
blanchet [Mon, 06 Jun 2011 20:36:35 +0200] rev 43181
don't stumble on Skolem names