changeset 50138 | ca989d793b34 |
parent 50132 | 180d086c30dd |
child 50139 | 7eb626617bbe |
--- a/NEWS Tue Nov 20 22:53:59 2012 +0100 +++ b/NEWS Wed Nov 21 09:07:41 2012 +0100 @@ -212,6 +212,8 @@ from sorted associative lists. Merging two trees with rbt_union may return a structurally different tree than before. MINOR INCOMPATIBILITY. +* Library/IArray.thy: immutable arrays with code generation. + * Simproc "finite_Collect" rewrites set comprehensions into pointfree expressions.