Re: [isabelle] Incompleteness and Nominal2


With the following download links I was successful (14.06.2015):

Kind regards,

Ken Kubota

> Am 07.07.2015 um 17:43 schrieb Manuel Eberl <eberlm at>:
> Hallo,
> 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.
> Cheers,
> Manuel

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