Wed, 06 Jun 2012 10:35:05 +0200 blanchet tweak Metis example to avoid glitch in proof reconstruction with a few guard-based, type-argument-less encodings
Wed, 06 Jun 2012 10:35:05 +0200 blanchet pass more facts to LEO-II, in the light of latest evaluation
Wed, 06 Jun 2012 10:35:05 +0200 blanchet prevent an "Empty" exception (e.g. with Satallax, "mono_native")
Wed, 06 Jun 2012 10:35:05 +0200 blanchet tuning terminology
Wed, 06 Jun 2012 10:35:05 +0200 blanchet updated NEWS
Wed, 06 Jun 2012 10:35:05 +0200 blanchet updated docs
Wed, 06 Jun 2012 10:35:05 +0200 blanchet added "args_query" encodings
Wed, 06 Jun 2012 10:35:05 +0200 blanchet removed killed encodings from Metis examples
Wed, 06 Jun 2012 10:35:05 +0200 blanchet updated docs
Wed, 06 Jun 2012 10:35:05 +0200 blanchet killed most unsound encodings
Wed, 06 Jun 2012 10:35:05 +0200 blanchet generalized monotonic constructor optimisation so that it works with e.g. the product type
Wed, 06 Jun 2012 10:35:05 +0200 blanchet removed micro-optimization whose justification I can't recall
Wed, 06 Jun 2012 10:35:05 +0200 blanchet add missing timeout multiplier
Wed, 06 Jun 2012 10:35:05 +0200 blanchet avoid dumping definitions several times in LEO-II proofs
(0) -30000 -10000 -3000 -1000 -300 -100 -14 +14 +100 +300 +1000 +3000 +10000 +30000 tip