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

[Andreas Lochbihler]

See now 8b7508f848ef. Library/Lattice_Constructions contains the remains of 
Library/Quickcheck_Types.

Andreas

On 18/08/14 18:44, Peter Lammich wrote:
>> 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
> HOL/Library/Lattice_Constructions.
>
> --
>    Peter
>
>
>