Re: [isabelle] Theory name conflict

> 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?

In principle, yes.  But it is a complication and cluttering, no

Let us again revisit the actual situation:


If I understand correctly, the problem is that fact names (also constant
names?) in Collections shadow some in Imperative_HOL.  My intention is
to refrain from any modification of the existing theories if there is
»natural« way to do so.

So maybe a user-space workaround is an intermediate theory

theory Heap_Array
imports "~~/src/HOL/Imperative_HOL/Array"

lemmas xyz =



and then in the main theory the imports


which would allow to access the facts mirrored in Heap_Array by

Would this solve your issue?

Hope this helps,



PGP available:

Attachment: signature.asc
Description: OpenPGP digital signature

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