Re: [isabelle] AFP Incompleteness Entry



On 2016-09-17 22:29, Gerwin.Klein at data61.csiro.au wrote:
> Hi Corey,
> 
> I canât reproduce the errors â if I download afp-2016-09-09, untar, and load up the theory Goedel_I in jedit/Isabelle2016 it processes fine, including the theories from Nominal2.
> 
> Is it possible that it is loading a wrong Nominal2 package from somewhere else, i.e. from an image?
> 

It's certainly possible, and it seems that was indeed the issue. Using
the HOL heap instead of HOL-Library yields success for me. Perhaps this
caveat should be mentioned on the AFP site? It seems like the root of
the issue here is some difference with multiset (at least, the first
error I got in Nominal2_Base was the instance of multiset :: (pt) pt).

Thanks for the help, regardless!

Best,
Corey


Attachment: signature.asc
Description: OpenPGP digital signature



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