Re: [isabelle] AFP Incompleteness Entry

was renamed in 003622e08379: resolve the name clash of HOL/Library/FSet and HOL/Quotient_Examples/FSet


On 09/19/2016 11:59 PM, Gerwin.Klein at wrote:
As long as the name clash exists in Isabelle itself, the issue will potentially reappear in other developments, though, so we should do something more permanent about it.


On 20.09.2016, at 03:10, OndÅej KunÄar <kuncar at> wrote:

Actually, this limitation of Nominal2 in AFP was already solved in
AFP/c515e20878fe: to be able to use the more standard Library/FSet.thy, rather than Quotient_Examples/FSet.thy (patch by Joachim Breitner)


On 09/18/2016 06:35 AM, Gerwin.Klein at wrote:
Turns out there is already a comment in Nominal2/ROOT:

   (* cannot depend on HOL-Library image because of name clash with Library/FSet: *)

Thatâs certainly more than a little inconvenient.

One of the two theories HOL/Library/FSet and HOL/Quotient_Examples/FSet should be renamed. This is not really an issue with the AFP, but with the Isabelle distribution itself.

Who are the guardians of these two?


On 18.09.2016, at 12:58, Corey Richardson <corey at> wrote:

On 2016-09-17 22:29, Gerwin.Klein at 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!


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