[isabelle-dev] (Re-)introducing set as a type constructor rather than as mere abbreviation

[Brian Huffman]

On Thu, Aug 11, 2011 at 5:43 AM, Florian Haftmann
<florian.haftmann at informatik.tu-muenchen.de> 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