Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] Isabelle theory name clash

view this post on Zulip Email Gateway (Jul 12 2026 at 21:20):

From: Zili Wang <ziliwang271@gmail.com>

Dear list,

I am interested in working with the Propositional_Proof_Systems and
SATSolverVerification
together, by the CNF file of the two sessions clash. Here is a minimal file
to recreate the issue:

CNF_clash.thy
'''
theory CNF_clash

imports
Propositional_Proof_Systems.CNF
SATSolverVerification.CNF

begin

end
'''

Output:
"exception THEORY raised (line 383 of "context.ML"):
Duplicate theory name
{..., Main, HOL-Library.Cancellation, HOL-Library.Multiset,
SATSolverVerification.MoreList, CNF}
{..., HOL.Binomial, Main, HOL-Library.Case_Converter,
HOL-Library.Simps_Case_Conv, CNF}"

What is the suggested workaround for importing both formalizations
simultaneously? I am using the latest AFP and Isabelle.

Thanks,
Zili

view this post on Zulip Email Gateway (Jul 13 2026 at 08:12):

From: Tobias Nipkow <nipkow@in.tum.de>

Hi Zili,

Unless you can import stuff selectively and avoid importing both CNF theories, I
think you will have to go in and modify the theory names by hand. The authors of
the two entries will in parallel liaise and modify their entries in the
development version of the AFP.

Thanks for the notification
Tobias

On 12/07/2026 23:19, Zili Wang wrote:

Dear list,

I am interested in working with the Propositional_Proof_Systems and
SATSolverVerification together, by the CNF file of the two sessions clash. Here
is a minimal file to recreate the issue:

CNF_clash.thy
'''
theory CNF_clash

imports
Propositional_Proof_Systems.CNF
SATSolverVerification.CNF

begin

end
'''

Output:
"exception THEORY raised (line 383 of "context.ML"):
  Duplicate theory name
  {..., Main, HOL-Library.Cancellation, HOL-Library.Multiset,
SATSolverVerification.MoreList, CNF}
  {..., HOL.Binomial, Main, HOL-Library.Case_Converter, HOL-
Library.Simps_Case_Conv, CNF}"

What is the suggested workaround for importing both formalizations
simultaneously? I am using the latest AFP and Isabelle.

Thanks,
Zili

smime.p7s

Last updated: Jul 23 2026 at 14:05 UTC