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