Re: [isabelle] Theory name conflict
On Wed, 5 Jan 2011, Florian Haftmann wrote:
No. The problem is that you simply cannot load two theories of the same
Try the following:
Interestingly, you don't even get an error, but the second theory is
silently ignored but not loaded.
This is a known feature of theory import paths, which have been added as
an afterthought some years ago, and never really worked. Stay tuned until
we get proper sessions with theory name spaces.
on its own works – not that I would call that a well-defined behaviour.
This looks strange, and should not import two different "Array" theories.
Which Isabelle version is this actually?
This archive was generated by a fusion of
Pipermail (Mailman edition) and