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"

  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.


  theory Scratch
  imports "~~/src/HOL/Imperative_HOL/Imperative_HOL"

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?


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