Re: [isabelle] Incompleteness and Nominal2

How about downloading it from the official Nominal Isabelle site:

I don't know though if the incompleteness proof works with this version.

- Gergely
From: cl-isabelle-users-bounces at [cl-isabelle-users-bounces at] On Behalf Of Larry Paulson [lp15 at]
Sent: Tuesday, July 07, 2015 5:51 PM
To: Manuel Eberl
Cc: isabelle-users
Subject: Re: [isabelle] Incompleteness and Nominal2

This is weird. It is definitely in the mercurial repository, but it doesn’t appear as an individual entry. This means that you have to download the entire AFP, all 144 MB, if you want to get it. I think that this has been the situation for a considerable time.

It’s worth mentioning that Incompleteness takes several minutes to run, even on a fast machine.

Larry Paulson

> On 7 Jul 2015, at 16: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

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