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

[Christian Urban]

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