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
