NEWS
changeset 49481 818bf31759e7
parent 49388 1ffd5a055acf
child 49510 ba50d204095e
     1.1 --- a/NEWS	Thu Sep 20 17:17:20 2012 +0200
     1.2 +++ b/NEWS	Thu Sep 20 17:21:13 2012 +0200
     1.3 @@ -109,6 +109,13 @@
     1.4  * Library/Debug.thy and Library/Parallel.thy: debugging and parallel
     1.5  execution for code generated towards Isabelle/ML.
     1.6  
     1.7 +* Library/FinFun.thy: theory of almost everywhere constant functions
     1.8 +(supersedes the AFP entry "Code Generation for Functions as Data").
     1.9 +
    1.10 +* Library/Phantom.thy: generic phantom type to make a type parameter
    1.11 +appear in a constant's type. This alternative to adding TYPE('a) as
    1.12 +another parameter avoids unnecessary closures in generated code.
    1.13 +
    1.14  * Simproc "finite_Collect" rewrites set comprehensions into pointfree
    1.15  expressions.
    1.16