| changeset 50634 | 009a9fdabbad |
| parent 50616 | 5b6cf0fbc329 |
| child 50645 | cb8f93361e86 |
--- a/NEWS Fri Dec 28 23:31:51 2012 +0100 +++ b/NEWS Sat Dec 29 17:18:01 2012 +0100 @@ -308,6 +308,8 @@ * Library/IArray.thy: immutable arrays with code generation. +* Library/Finite_Lattice.thy: theory of finite lattices + * Simproc "finite_Collect" rewrites set comprehensions into pointfree expressions.