[isabelle-dev] sets and code generation
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
> 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