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
B.My_Theory disambiguated by session namespace business. This doesn't seem to be the case?...
Relevant mailing list links:
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: Aug 15 2022 at 02:13 UTC