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.

Kind regards,
René

PS: We are currently depending on 14 AFP-entries.



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.