Josh Chen (Jul 31 2020 at 09:07): Josh Chen (Jul 31 2020 at 09:07):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.
Josh Chen (Jul 31 2020 at 09:12):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.
Mathias Fleury (Jul 31 2020 at 11:42):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 21 2024 at 12:33 UTC