Re: [isabelle] Theory name conflict



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.

No. The problem is that you simply cannot load two theories of the same name.

Try the following:

  theory Scratch
  imports "~~/src/HOL/Imperative_HOL/Array"
    "$PATH_TO_AFP/Collections/common/Array"
  begin

  term array_of_list

Interestingly, you don't even get an error, but the second theory is silently ignored but not loaded.

Alex





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