[isabelle-dev] (Re-)introducing set as a type constructor rather than as mere abbreviation
brianh at cs.pdx.edu
Thu Aug 11 17:11:40 CEST 2011
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".
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
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
More information about the isabelle-dev