On 04/04/17 11:06, Manuel Eberl wrote:
> During a minor overhaul of some theories in the distribution, I
> discovered some problems with theory imports.
>
> In short: apparently, importing a theory (e.g. Library/Multiset) twice
> in two theories A and B can be problematic when the theory import is
I forgot to mention the changeset ID. The problem occurs in
d32e702d7ab8, but I don't think that's the earliest changeset that
exhibits these problems.
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mail
During a minor overhaul of some theories in the distribution, I
discovered some problems with theory imports.
Apparently, the theory merge behaviour changed in one of the most recent
commits. I haven't been able to pin down which one it is exactly; I
might do a bisection later if needed.
In short
