Mon, 06 Jun 2011 20:36:35 +0200 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 43195
improved correctness of handling of higher-order occurrences of "Not" in new Metis (and probably in old Metis)
Mon, 06 Jun 2011 20:36:35 +0200 fixed type helper indices in new Metis
blanchet [Mon, 06 Jun 2011 20:36:35 +0200] rev 43194
fixed type helper indices in new Metis
Mon, 06 Jun 2011 20:36:35 +0200 improved ATP clausifier so it can deal with "x => (y <=> z)"
blanchet [Mon, 06 Jun 2011 20:36:35 +0200] rev 43193
improved ATP clausifier so it can deal with "x => (y <=> z)"
Mon, 06 Jun 2011 20:36:35 +0200 avoid renumbering hypotheses
blanchet [Mon, 06 Jun 2011 20:36:35 +0200] rev 43192
avoid renumbering hypotheses
Mon, 06 Jun 2011 20:36:35 +0200 fixed reconstruction of new Skolem constants in new Metis
blanchet [Mon, 06 Jun 2011 20:36:35 +0200] rev 43191
fixed reconstruction of new Skolem constants in new Metis
Mon, 06 Jun 2011 20:36:35 +0200 don't translate new Skolemizer assumptions in new Metis
blanchet [Mon, 06 Jun 2011 20:36:35 +0200] rev 43190
don't translate new Skolemizer assumptions in new Metis
Mon, 06 Jun 2011 20:36:35 +0200 tuning
blanchet [Mon, 06 Jun 2011 20:36:35 +0200] rev 43189
tuning
Mon, 06 Jun 2011 20:36:35 +0200 fixed detection of Skolem constants in type construction detection code
blanchet [Mon, 06 Jun 2011 20:36:35 +0200] rev 43188
fixed detection of Skolem constants in type construction detection code
Mon, 06 Jun 2011 20:36:35 +0200 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 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)
Mon, 06 Jun 2011 20:36:35 +0200 tuning
blanchet [Mon, 06 Jun 2011 20:36:35 +0200] rev 43186
tuning
(0) -30000 -10000 -3000 -1000 -300 -100 -10 +10 +100 +300 +1000 +3000 +10000 +30000 tip