Quoting Florian Haftmann <florian.haftm...@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 _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
