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

Peter Lammich lammich at in.tum.de
Mon Aug 18 18:44:15 CEST 2014

> However, the constructions might still be useful, as the following comment from Peter 
> Lammich's AFP entry Refine_Monadic shows.
>    (* TODO: Library/Quickcheck_Types.thy:flat_complete_lattice provides
>      an isomorphic contruction. *)

At this point I duplicated the flat complete lattice construction
locally, as I did not want to use rely on a construction from such a
special and unrelated thing as quickcheck.

> So, should we keep Quickcheck_Types (maybe under a different name, say 
> Lattice_Constructions) or drop it?

I think, at least the "standard" constructions, like flat complete
lattice, should be preserved and either directly go into
Complete_Lattice or, as you proposed, into


More information about the isabelle-dev mailing list