Re: [isabelle] Incompleteness and Nominal2

Whatâs going on is that Nominal2 is not an official entry, so has no website entry and no separate tar file to download.

Nominal2 was supposed to go into the Isabelle distribution and replace Nominal. This has not happened in over a year, and Iâm not happy with this situation. It should either become a real entry or be removed.

Currently, the best way to get it is to download the whole AFP release (from the download link in the navigation panel on the left).


> On 8 Jul 2015, at 01:43, Manuel Eberl <eberlm at> wrote:
> 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


The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.

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