Re: [isabelle] Theory name conflict



Le mardi 18 janvier 2011 11:10:32, Alexander Krauss a écrit :
> Mathieu Giorgino wrote:
> > It's still the same. Reading this:
> >   theory Scratch
> >   
> >     imports
> >     "~~/src/HOL/Imperative_HOL/Array"
> >     "/home/giorgino/repos/afp/thys/Collections/common/Array"
> >   
> >   begin
> > 
> > or this:
> >   theory Scratch
> >   
> >     imports
> >     "~~/src/HOL/Imperative_HOL/Array"
> >     "/non/existing/path/Array"
> >     "a/relative/non/existing/path/Array"
> >     "/home/giorgino/repos/afp/thys/Collections/common/Array"
> >   
> >   begin
> >   
> >   term Array
> > 
> > works like a charm.
> 
> What do you mean with "works like a charm". What is the behaviour you
> see? I would expect that the declaration is accepted but the second
> theory is not loaded. Is that correct? If yes, "works like a charm" is a
> bit of a euphemism. If no, what happens exactly?
> 
> Alex

Yes, sorry... I mean that the declaration is accepted but the second theory is 
not loaded.

Mathieu





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