[isabelle] Incompleteness and Nominal2


Dana Scott just asked me why he could not get the AFP entry
Incompleteness to work. I tried it myself and found that the entry makes
use of Nominal2, but Nominal2 is not an AFP entry itself, nor is it
available anywhere else. All I found is an old version that works with
Isabelle 2014.

Strangely, when clicking âBrowse theoriesâ in the Incompleteness AFP
entry, some Nominal2 theories show up, but when downloading the .tar.gz
(âDownload this entryâ), they are not in the archive.

What is the current status of Nominal2, especially in combination with
Incompleteness? Having an AFP entry online that does not work when you
download it and load it into Isabelle seems highly undesirable to me.



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.