[isabelle-dev] Dead and broken theory src/HOL/Library/Quickcheck_Types.thy

Makarius makarius at sketis.net
Fri Jul 11 15:44:28 CEST 2014

On Fri, 11 Jul 2014, Andreas Lochbihler wrote:

> If there's consensus on reviving this theory, I can do the changes to 
> Quickcheck_Types such that Isabelle2014 digests it. This is probably all 
> that can be done before the release as most of us will be busy in Vienna 
> next week. A move to Main is something for the next release.

I can't say anything myself how it would impact the bootstrap of Main HOL. 
As long as this question does not arise for the Isabelle2014 release, I 
would say: go ahead and renovate it.


More information about the isabelle-dev mailing list