Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] "Bad theory import" for conflicting theory names

view this post on Zulip Email Gateway (Aug 22 2022 at 14:02):

From: Bertram Felgenhauer via Cl-isabelle-users <cl-isabelle-users@lists.cam.ac.uk>
When trying to load a theory Fun.thy with the following contents,

theory Fun
imports "~~/src/HOL/Library/Multiset"
(* error: Bad theory import "Multiset" *)
begin
end

we get the indicated "Bad theory import" error message. Typically that
error indicates a wrong theory path, but in fact the path is correct
and the real problem is that the Multiset theory transitively depends
on a theory called Fun, and Isabelle(/Pure?) does not support having
multiple theories of the same name.

It would be helpful if the error message pointed out the conflicting
theory names.

Incidentally, if the Multiset theory is already loaded, the error
message changes to "Cannot update finished theory "Fun"" which is much
more helpful.

Cheers,

Bertram

Last updated: Nov 21 2024 at 12:39 UTC