Re: [isabelle] AFP Incompleteness Entry



Would work for me!

Cheers,
Gerwin

> On 18.09.2016, at 22:43, OndÅej KunÄar <kuncar at in.tum.de> wrote:
> 
> 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.