[isabelle-dev] Quickcheck Examples

[Lukas Bulwahn]

On 02/18/2012 10:18 AM, Florian Haftmann wrote:
>> How much relative time do the quickcheck examples in HOL-ex take?
>> According to my feeling time could be high to separate these into a
>> separate session, to facilitate maintenance.
> Are there any voices pro or contra?  IMHO the overhead when figuring out
> (frequently occurring) non-termination problems in HOL-ex is not
> tolerable at the moment, so a fat cure would be reasonable.
I guess there are no voices at all. If you have strong feelings for yet 
another session, I can go ahead and split the theories.


Lukas