Re: [isabelle] Theory name conflict

Let us again revisit the actual situation:


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"

  term array_of_list

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


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