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.

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.

	Florian

-- 

Home:
http://www.in.tum.de/~haftmann

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

Attachment: signature.asc
Description: OpenPGP digital signature



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