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 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

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

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

I wonder if there are more old theories like that.


Attachment: signature.asc
Description: OpenPGP digital signature

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