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?

Cheers,
Gerwin

> On 18.09.2016, at 11:32, Klein, Gerwin (Data61, Kensington NSW) <Gerwin.Klein at data61.csiro.au> 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 octayn.net> 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.