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


More information about the isabelle-dev mailing list