Re: [isabelle] Theory name conflict



On Wed, 5 Jan 2011, Florian Haftmann wrote:

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.

This is a known feature of theory import paths, which have been added as an afterthought some years ago, and never really worked. Stay tuned until we get proper sessions with theory name spaces.


But

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

on its own works – not that I would call that a well-defined behaviour.

This looks strange, and should not import two different "Array" theories. Which Isabelle version is this actually?


	Makarius


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