Re: [isabelle] AFP Incompleteness Entry



> On 18.09.2016, at 06:35, Gerwin.Klein at data61.csiro.au wrote:
> 
> Turns out there is already a comment in Nominal2/ROOT:
> 
>    (* cannot depend on HOL-Library image because of name clash with Library/FSet: *)
>    "~~/src/HOL/Quotient_Examples/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?

The Quotient_Examples version is clearly the one that should be renamed. Judging from the logs, it was developed by Cezary Kaliszyk, then semi-obsoleted by Ondra Kuncar who developed the new FSet in Library. See e.g. Isabelle/9a21e5c6e5d9. Perhaps we should simply rename the old, example "FSet" to "Old_FSet"? This would be consistent with this warning:

(********************************************************************
  WARNING: There is a formalization of 'a fset as a subtype of sets in
  HOL/Library/FSet.thy using Lifting/Transfer. The user should use
  that file rather than this file unless there are some very specific
  reasons.
*********************************************************************)

Jasmin





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