Dear all, 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, it seems that the second theory file "unloads" the first one (as Makarius suggested in his mail):
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? Thanks for your help, Jesus On Fri, Mar 23, 2012 at 1:25 PM, Makarius <makar...@sketis.net> wrote: > On Fri, 23 Mar 2012, Christian Sternagel wrote: > >> Maybe the AFP entry for executable matrix operations is useful for you. >> >> http://afp.sourceforge.net/entries/Matrix.shtml >> >>> (HOL/Matrix/Matrix.thy). > > > Note that in current Isabelle/08c22e8ffe70 HOL/Matrix is actually called > HOL/Matrix_LP, in order to avoid a name clash of the AFP/HOL-Matrix session > (the latter was introduced later, but AFP names are not so easy to change as > I understand it). > > Technically, the motivation is to get globally unique session names for > official Isabelle + AFP sessions. Then when we eventually get a decent > build system (based on Isabelle/Scala), the user can refer to sessions > robustly without tinkering IsaMakefiles or funny search paths. > > > Makarius > > _______________________________________________ > isabelle-dev mailing list > isabelle-...@in.tum.de > https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev -- Jesús María Aransay Azofra Universidad de La Rioja Dpto. de Matemáticas y Computación tlf.: (+34) 941299438 fax: (+34) 941299460 mail: jesus-maria.aran...@unirioja.es ; web: http://www.unirioja.es/cu/jearansa Edificio Luis Vives, c/ Luis de Ulloa s/n, 26004 Logroño, España _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev