[isabelle-dev] sets and code generation
makarius at sketis.net
Fri Mar 23 13:25:33 CET 2012
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.
More information about the isabelle-dev