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