Re: [isabelle] Theory name conflict
Is there an easy "user side" way to get rid of it without renaming one of
Yes... it's a known (and very annoying when you hit it) limitation of
the current flat theory namespace.
@Peter: maybe we should consider renaming one of these, e.g.
~~/src/HOL/Imperative_HOL/Array.thy to Arr.thy. But I do not see a
natural choice here, maybe you do.
Making the name shorter will inevitably provoke new conflicts. If you
change it, make it longer, e.g. Heap_Array. Users usually don't import
this theory individually, only the via Imperative_HOL entry point.
But I now see that the theory name is intended as a qualifier for
constants... Could one achieve this behavior using other means, e.g., a
vacuous locale or something?
This archive was generated by a fusion of
Pipermail (Mailman edition) and