[isabelle-dev] sets and code generation
jesus-maria.aransay at unirioja.es
Tue Mar 27 18:36:49 CEST 2012
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):
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,
On Fri, Mar 23, 2012 at 1:25 PM, Makarius <makarius at sketis.net> wrote:
> On Fri, 23 Mar 2012, Christian Sternagel wrote:
>> Maybe the AFP entry for executable matrix operations is useful for you.
> 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.
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
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.aransay at unirioja.es ; web: http://www.unirioja.es/cu/jearansa
Edificio Luis Vives, c/ Luis de Ulloa s/n, 26004 Logroño, España
More information about the isabelle-dev