Re: [isabelle] AFP Incompleteness Entry
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 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.
>> 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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and