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
Try the following:
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