Re: [isabelle] Theory name conflict

> 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.


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

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




PGP available:

Attachment: signature.asc
Description: OpenPGP digital signature

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