Hi Andreas, Am 14.03.2014 um 15:26 schrieb Andreas Lochbihler <andreas.lochbih...@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. Jasmin _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
