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
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
