[isabelle-dev] sets and code generation

[Makarius]

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