[isabelle-dev] smt2

Jasmin Blanchette jasmin.blanchette at gmail.com
Fri Mar 14 16:05:21 CET 2014

Hi Andreas,

Am 14.03.2014 um 15:26 schrieb Andreas Lochbihler <andreas.lochbihler at inf.ethz.ch>:

> On 14/03/14 14:18, Jasmin Blanchette wrote:
>> Another candidate is "Quickcheck_Narrowing.thy". Nothing in "HOL" seems to depend on it, and (please correct me if I'm mistaken) hardly anybody go into the trouble of setting up Quickcheck (and GHC) so that it uses the narrowing strategy.
> I guess I am the exception to the rule. I have GHC set up and sometimes try quickcheck[narrowing]. Sometimes, it does give better results than the random and exhaustive generators.

How big an issue is it to you if we move narrowing to Library? From what I understand, you already pull in quite a bit from Library, to the extent that "Coinductive" is based on the "HOL-Library" session. And Quickcheck has a nice generic interface for registering "testers" at any point, so technically the move should be nearly trivial.


More information about the isabelle-dev mailing list