Re: [isabelle] Incompleteness and Nominal2



Hello,

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

	http://www.cl.cam.ac.uk/research/hvg/Isabelle/dist/Isabelle2015.dmg
	http://sourceforge.net/projects/afp/files/afp-Isabelle2015/afp-2015-05-28.tar.gz/download

Kind regards,

Ken Kubota


> Am 07.07.2015 um 17:43 schrieb Manuel Eberl <eberlm at in.tum.de>:
> 
> 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.