Re: [isabelle] theory FSet exists twice



On 23/06/16 18:08, Joachim Breitner wrote:
> Iâm trying to use Nominal2 (as shipped in AFP-2016) in a theory that
> also uses  "~~/src/HOL/Library/FSet". This leads to
> 
> exception THEORY raised (line 221 of "context.ML"):
>   Duplicate theory name
>   {..., BNF_Greatest_Fixpoint, Filter, Main, Conditionally_Complete_Lattices, FSet}
>   {..., Quotient_Product, Quotient_Option, Multiset, Quotient_List, FSet}
> 
> The problem seems to be that Nominal2_Base imports
> "~~/src/HOL/Quotient_Examples/FSet".
> 
> Can I work around this problem without modifying HOL or Nominal2?
> 
> Also, should the ~~/src/HOL/Quotient_Examples/FSet theory be renamed to
> avoid this problem?

The changeset
http://isabelle.in.tum.de/repos/isabelle/rev/9a21e5c6e5d9 adds a comment
as follows:

  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.

And the change log says: "declare Quotient_Examples/FSet.thy as almost
obsolete".

So it looks like Quotient_Examples/FSet.thy should be renamed to
Quotient_Examples/FSet_Old.thy

I wonder if there are more old theories like that.


	Makarius




Attachment: signature.asc
Description: OpenPGP digital signature



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