Re: [isabelle] Theory name conflict



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





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