equal
deleted
inserted
replaced
209 another parameter avoids unnecessary closures in generated code. |
209 another parameter avoids unnecessary closures in generated code. |
210 |
210 |
211 * Library/RBT_Impl.thy: efficient construction of red-black trees |
211 * Library/RBT_Impl.thy: efficient construction of red-black trees |
212 from sorted associative lists. Merging two trees with rbt_union may |
212 from sorted associative lists. Merging two trees with rbt_union may |
213 return a structurally different tree than before. MINOR INCOMPATIBILITY. |
213 return a structurally different tree than before. MINOR INCOMPATIBILITY. |
|
214 |
|
215 * Library/IArray.thy: immutable arrays with code generation. |
214 |
216 |
215 * Simproc "finite_Collect" rewrites set comprehensions into pointfree |
217 * Simproc "finite_Collect" rewrites set comprehensions into pointfree |
216 expressions. |
218 expressions. |
217 |
219 |
218 * Preprocessing of the code generator rewrites set comprehensions into |
220 * Preprocessing of the code generator rewrites set comprehensions into |