[isabelle-dev] smt2

[Andreas Lochbihler]

Hi Jasmin,


On 14/03/14 16:05, Jasmin Blanchette wrote:
> 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?
I don't mind if narrowing is moved to HOL-Library, I'll just add another theory to my list 
of theories that I usually import. If you do so, please make sure that the connection to 
the datatype packages is kept, i.e., narrowing generators are generated for all datatypes 
(even those that are defined while narrowing was not in scope).

 >  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.

IIRC, the AFP policy is (was?) that all entries that import at least one theory from 
HOL-Library are based on HOL-Library.

Andreas