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
Mon, 06 Jun 2011 20:36:35 +0200 also exploit type tag idempotence in lightweight encodings, following a suggestion from Gothenburg
blanchet [Mon, 06 Jun 2011 20:36:35 +0200] rev 43185
also exploit type tag idempotence in lightweight encodings, following a suggestion from Gothenburg
Mon, 06 Jun 2011 20:36:35 +0200 reveal Skolems in new Metis
blanchet [Mon, 06 Jun 2011 20:36:35 +0200] rev 43184
reveal Skolems in new Metis
Mon, 06 Jun 2011 20:36:35 +0200 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 43183
don't throw exception on unknown constants (e.g. skolems), and give more precise type to applied functions
Mon, 06 Jun 2011 20:36:35 +0200 slacker version of "fastype_of", in case a function has dummy type
blanchet [Mon, 06 Jun 2011 20:36:35 +0200] rev 43182
slacker version of "fastype_of", in case a function has dummy type
Mon, 06 Jun 2011 20:36:35 +0200 don't stumble on Skolem names
blanchet [Mon, 06 Jun 2011 20:36:35 +0200] rev 43181
don't stumble on Skolem names
Mon, 06 Jun 2011 20:36:35 +0200 conceal old Skolems in new Metis
blanchet [Mon, 06 Jun 2011 20:36:35 +0200] rev 43180
conceal old Skolems in new Metis
(0) -30000 -10000 -3000 -1000 -300 -100 -10 +10 +100 +300 +1000 +3000 +10000 tip