Re: [isabelle] Theory name conflict

Is there an easy "user side" way to get rid of it without renaming one of them?

unfortunately, not.

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 MHonArc.