Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] theory FSet exists twice

view this post on Zulip Email Gateway (Aug 22 2022 at 13:27):

From: Joachim Breitner <breitner@kit.edu>
Hi list,

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?

Thanks,
Joachim
signature.asc

view this post on Zulip Email Gateway (Aug 22 2022 at 13:40):

From: Makarius <makarius@sketis.net>
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
signature.asc

Last updated: Apr 25 2024 at 20:15 UTC