blanchet [Mon, 06 Jun 2011 20:36:35 +0200] rev 44042
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 44041
imported patch metis_reconstr_give_type_infer_a_chance
blanchet [Mon, 06 Jun 2011 20:36:35 +0200] rev 44040
make "metisX"'s default more like old "metis"
blanchet [Mon, 06 Jun 2011 20:36:35 +0200] rev 44039
whitespace tuning
blanchet [Mon, 06 Jun 2011 20:36:35 +0200] rev 44038
tuned Metis examples
blanchet [Mon, 06 Jun 2011 20:36:35 +0200] rev 44037
more through tests of new Metis
blanchet [Mon, 06 Jun 2011 20:36:35 +0200] rev 44036
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 44035
fixed type helper indices in new Metis
blanchet [Mon, 06 Jun 2011 20:36:35 +0200] rev 44034
improved ATP clausifier so it can deal with "x => (y <=> z)"
blanchet [Mon, 06 Jun 2011 20:36:35 +0200] rev 44033
avoid renumbering hypotheses