If session B imports session A which has theory My_Theory
, I would expect to be able to create a new theory file with the same name in B, and have both A.My_Theory
and B.My_Theory
disambiguated by session namespace business. This doesn't seem to be the case?...
Relevant mailing list links:
https://lists.cam.ac.uk/mailman/htdig/cl-isabelle-users/2020-March/msg00001.html
https://lists.cam.ac.uk/mailman/htdig/cl-isabelle-users/2011-January/msg00003.html
Still not fixed since 2011, I see.
I found the answer on the mailing list after I wrote the first post (which, as so many other things, seems to be just "it can't be done"...), but I'll leave this up here for newcomers.
This is one reason why the AFP contains a Multiset_More, a Missing_Multiset, a Missing_Multiset2, a multisets_continued (sic), and a Multiset_Extension: You want a new name each time
Last updated: Dec 07 2024 at 16:22 UTC