Re: [isabelle] Name clashes in theory names
>> Seconded. I also ran into this problem a few times.
> Me too.
Thanks for your agreements.
> For me, its an indication that Isabelle's simple name-space model is not
> adequate for programming in the large, but it is exactly that what we do
> in some of our developments, depending on >10 AFP-entries.
Indeed, a more structured name-space model would of course be most welcome,
but I imagine this would be a larger effort than just a adding a warning message.
PS: We are currently depending on 14 AFP-entries.
This archive was generated by a fusion of
Pipermail (Mailman edition) and