[isabelle-dev] sets and code generation

Makarius makarius at sketis.net
Tue Apr 10 11:22:32 CEST 2012


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


More information about the isabelle-dev mailing list