[isabelle-dev] sets and code generation

[Jesus Aransay]

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 <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.
>>
>> 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-dev at 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.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