isabelle: Changelog

blanchet [Mon, 06 Jun 2011 20:36:34 +0200] rev 43167

ensured that the logic for "explicit_apply = smart" also works on CNF (i.e. new Metis)

blanchet [Mon, 06 Jun 2011 20:36:34 +0200] rev 43166

show what failed to play

blanchet [Mon, 06 Jun 2011 20:36:34 +0200] rev 43165

refined auto minimization code: don't use Metis if Isar proofs are desired, and fall back on prover if Metis is too slow

blanchet [Mon, 06 Jun 2011 20:36:34 +0200] rev 43164

tuning

blanchet [Mon, 06 Jun 2011 20:36:34 +0200] rev 43163

killed odd connectives

blanchet [Mon, 06 Jun 2011 20:36:34 +0200] rev 43162

added Metis examples to test the new type encodings

blanchet [Mon, 06 Jun 2011 20:36:34 +0200] rev 43161

tuned CASC method

blanchet [Mon, 06 Jun 2011 20:36:34 +0200] rev 43160

clean up unnecessary machinery -- helpers work also with monomorphic type encodings

blanchet [Mon, 06 Jun 2011 20:36:34 +0200] rev 43159

added support for helpers in new Metis, so far only for polymorphic type encodings

kleing [Mon, 06 Jun 2011 16:29:38 +0200] rev 43158

imported rest of new IMP

isabelle