[isabelle-dev] (Re-)introducing set as a type constructor rather than as mere abbreviation
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.
More information about the isabelle-dev