blanchet [Mon, 06 Jun 2011 20:36:35 +0200] rev 43176
only uncombine combinators in textual Isar proofs, not in Metis
blanchet [Mon, 06 Jun 2011 20:36:35 +0200] rev 43175
properly locate helpers whose constants have several entries in the helper table
blanchet [Mon, 06 Jun 2011 20:36:35 +0200] rev 43174
skip "hBOOL" in new Metis path finder
blanchet [Mon, 06 Jun 2011 20:36:35 +0200] rev 43173
don't pass "~ " to new Metis
blanchet [Mon, 06 Jun 2011 20:36:35 +0200] rev 43172
tuning
blanchet [Mon, 06 Jun 2011 20:36:35 +0200] rev 43171
gracefully handle the case where a constant is partially or not instantiated at all, as may happen when reconstructing Metis proofs for polymorphic type encodings
blanchet [Mon, 06 Jun 2011 20:36:35 +0200] rev 43170
temporarily document "metisX"
blanchet [Mon, 06 Jun 2011 20:36:34 +0200] rev 43169
use "metisX" as fallback, since it's much faster than "metisFT"
blanchet [Mon, 06 Jun 2011 20:36:34 +0200] rev 43168
temporarily added "MetisX" as reconstructor and minimizer
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
kleing [Mon, 06 Jun 2011 16:29:13 +0200] rev 43157
atLeastAtMostSuc_conv on int
kleing [Mon, 06 Jun 2011 14:11:54 +0200] rev 43156
fixed typo
boehmes [Sun, 05 Jun 2011 15:00:52 +0200] rev 43155
updated SMT certificates
boehmes [Sun, 05 Jun 2011 15:00:17 +0200] rev 43154
made introduction of explicit application stable under removal of vacuous facts (which only lower the rank of constants but do not participate in the proof)
bulwahn [Fri, 03 Jun 2011 19:37:26 +0200] rev 43153
changing the mira setting again for the mutabelle configuration
bulwahn [Fri, 03 Jun 2011 07:25:44 +0200] rev 43152
adding more settings to mira's mutabelle configuration
nipkow [Thu, 02 Jun 2011 15:17:23 +0200] rev 43151
merged
nipkow [Thu, 02 Jun 2011 10:10:23 +0200] rev 43150
Added typed IMP
bulwahn [Thu, 02 Jun 2011 10:13:46 +0200] rev 43149
adding quickcheck narrowing to mutabelle script; deactivating nitpick in mutabelle script momentarily because we are not monitoring the results effectively
bulwahn [Thu, 02 Jun 2011 09:51:40 +0200] rev 43148
adding invocation of exhaustive testing without using finite types to mutabelle
bulwahn [Thu, 02 Jun 2011 09:51:40 +0200] rev 43147
moving the distinction between invocation of testers and generators into test_goal_terms function in quickcheck for its usage with mutabelle