Re: [isabelle] Theory name conflict
I've been too long to answer but it could anyway explain a little more the
> 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.
In fact, all objects defined or imported by the last in the import list (the
last read theory ?) are hidden.
For example, in the reverse situation:
where "Imperative_HOL/Array" imports "Heap_Monad" which imports "Heap",
typ "'a Heap_Monad.Heap"
are all hidden, and so trying to import this:
"~~/src/HOL/Imperative_HOL/Ref" (* where Ref imports Array*)
results in errors, as "Ref" uses the type "Heap.heap" and ArrayHashMap_Impl
uses constant "Array.array_get".
Then, it is impossible to import "Collections" (importing "ArrayHashMap_Impl")
and "Imperative_HOL" (importing "Ref") at the same time.
> So maybe a user-space workaround is an intermediate theory
> Would this solve your issue?
It would not solve the issue as the intermediate theory would have to be
inserted in "Collections" or "Imperative_HOL" and it would then be easier to
change one theory name.
I will try to import selectively theories "Ref" and "Mrec" of "Imperative_HOL"
as I don't use "Imperative_HOL" arrays anyway... but I could have...
I hope to see soon localization of theories...
Thank you both,
This archive was generated by a fusion of
Pipermail (Mailman edition) and