Re: [isabelle] AFP Incompleteness Entry



If nobody objects, I will rename Quotient_Examples/FSet to Quotient_Examples/Quotient_FSet.

Ondrej

On 09/18/2016 01:36 PM, Jasmin Blanchette wrote:

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.