Re: [isabelle] AFP Incompleteness Entry

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?


> On 18.09.2016, at 11:32, Klein, Gerwin (Data61, Kensington NSW) <Gerwin.Klein at> wrote:
> Let me investigate that. You shouldnât be getting any errors from Nominal2, esp not if it builds fine in batch mode.
> Cheers,
> Gerwin
>> On 18.09.2016, at 09:57, Corey Richardson <corey at> wrote:
>> Greetings AFP maintainers,
>> Using the 2016-09-09 release of the AFP, I have tried exploring the
>> Incompleteness entry with Isabelle2016. The sessions of that directory
>> build fine with "isabelle build", but when I try to open Goedel_I.thy in
>> jEdit I get numerous errors from Nominal2. Is there a special way to
>> invoke jEdit that allows interactive exploration of these theories? I
>> especially find the control-click navigation useful.
>> Best,
>> Corey

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