> 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 _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
