Hi again,
thanks Alex for the summary.
So, it seems that we can conclude that instead of the nice unified
development that we hoped for in 2008, we got quite a bit of confusion
(points 1.1 and 1.2), in addition to the drawbacks that were already
known (1.3, 1.5-1.6). If we had to choose
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
