*To*: Joachim Breitner <breitner at kit.edu>, cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] theory FSet exists twice*From*: Makarius <makarius at sketis.net>*Date*: Mon, 25 Jul 2016 17:42:56 +0200*In-reply-to*: <1466698136.16347.14.camel@kit.edu>*References*: <1466698136.16347.14.camel@kit.edu>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:45.0) Gecko/20100101 Thunderbird/45.2.0

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

- Previous by Date: Re: [isabelle] Operator clash for $
- Next by Date: Re: [isabelle] qed and done take long for large goal states
- Previous by Thread: Re: [isabelle] Operator clash for $
- Next by Thread: [isabelle] Proposal: An update to Multiset theory
- Cl-isabelle-users July 2016 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list