[isabelle-dev] sets and code generation

[Makarius]

On Tue, 27 Mar 2012, Jesus Aransay wrote:

> trying to import simultaneously the theory file
> "HOL/Matrix/Matrix.thy" and the afp entry
> http://afp.sourceforge.net/entries/Matrix.shtml into a file
>
> theory Matrix_ex
>  imports
>  "~~/src/HOL/Matrix/Matrix"
>  "Matrix/Matrix"
> begin
>
> Is there an easy way out of this situation in Isabelle2011-1? Renaming 
> one of the theory files is an acceptable solution in this case?

Renaming one of the theory files (on your private copy) is the only 
solution in contemporary Isabelle.  It is acceptable, because it is just 
one file here.


 	Makarius