equal
deleted
inserted
replaced
377 |
377 |
378 * HOL/BNF: New (co)datatype package based on bounded natural functors |
378 * HOL/BNF: New (co)datatype package based on bounded natural functors |
379 with support for mixed, nested recursion and interesting non-free |
379 with support for mixed, nested recursion and interesting non-free |
380 datatypes. |
380 datatypes. |
381 |
381 |
382 * HOL/Finite_Set and Relation: added new set and relation operations |
382 * HOL/Finite_Set and Relation: added new set and relation operations |
383 expressed by Finite_Set.fold. |
383 expressed by Finite_Set.fold. |
384 |
384 |
385 * New theory HOL/Library/RBT_Set: implementation of sets by red-black |
385 * New theory HOL/Library/RBT_Set: implementation of sets by red-black |
386 trees for the code generator. |
386 trees for the code generator. |
387 |
387 |