On Thu, Aug 11, 2011 at 5:43 AM, Florian Haftmann <[email protected]> wrote: > Hello together, > > recently in some personal discussions the matter has arisen whether > there would be good reason to re-introduce the ancient set type > constructor. To open the discussion I have carried together some > arguments. I'm pretty sure there are further ones either pro or contra, > for which this mailing list seems a good place to collect them.
One of the arguments in favor of identifying "'a set" and "'a => bool" was for "compatibility with other HOLs". https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2008-December/msg00043.html If we make them into separate types again, how will tools that import proofs from other HOLs be affected? I am interested in this question because I have written such a tool myself (I hacked up an importer for Joe Hurd's OpenTheory format a while back). Florian: Is your modified Isabelle repo available for cloning, so we can play with it? If so, I might be able to find an answer to my own question... - Brian _______________________________________________ isabelle-dev mailing list [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
