*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] Theory name conflict*From*: Mathieu Giorgino <mathieu.giorgino at irit.fr>*Date*: Wed, 5 Jan 2011 13:35:03 +0100*In-reply-to*: <4D24507C.8040401@informatik.tu-muenchen.de>*Organization*: IRIT*References*: <201101032020.41577.mathieu.giorgino@irit.fr> <4D2449AF.8050403@in.tum.de> <4D24507C.8040401@informatik.tu-muenchen.de>*User-agent*: KMail/1.13.5 (Linux/2.6.36-ARCH; KDE/4.5.4; x86_64; ; )

I've been too long to answer but it could anyway explain a little more the problem. > Let us again revisit the actual situation: > > "~~/src/HOL/Imperative_HOL/Array" > "afp/thys/Collections/common/Array" > > 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: "afp/thys/Collections/common/Array" "~~/src/HOL/Imperative_HOL/Array" where "Imperative_HOL/Array" imports "Heap_Monad" which imports "Heap", term Array.get thm Array.noteq_sym term Heap_Monad.Heap typ "'a Heap_Monad.Heap" thm Heap.addr_of_array_inj typ Heap.heap term Heap.empty are all hidden, and so trying to import this: "afp/thys/Collections/common/Array" "~~/src/HOL/Imperative_HOL/Ref" (* where Ref imports Array*) or this: "~~/src/HOL/Imperative_HOL/Array" "afp/thys/Collections/common/ArrayHashMap_Impl" 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, Mathieu

**References**:**[isabelle] Theory name conflict***From:*Mathieu Giorgino

**Re: [isabelle] Theory name conflict***From:*Alexander Krauss

**Re: [isabelle] Theory name conflict***From:*Florian Haftmann

- Previous by Date: Re: [isabelle] How to show that locale loop is finite?
- Next by Date: Re: [isabelle] Using abbreviations with case expressions
- Previous by Thread: Re: [isabelle] Theory name conflict
- Next by Thread: [isabelle] Problem with istallation of Isabelle
- Cl-isabelle-users January 2011 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list