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