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

Christian Urban urbanc at in.tum.de
Sun Sep 4 00:02:02 CEST 2011


Quoting Florian Haftmann <florian.haftmann at informatik.tu-muenchen.de>:

> I will now examine HOL-Nominal more closer, and after that come up with
> a next report about the distribution.

There should be no problems in principle.
Early versions of Nominal (1) worked perfectly
with an explicit set-type. They had an instance
for sets and permutation types, and that is
basically the only Nominal specific change
that is needed now.

Best wishes,
Christian



More information about the isabelle-dev mailing list