NEWS
changeset 50991 b3c6c9ef11b8
parent 50878 2840522a936d
child 50993 2c3d0cb151c0
equal deleted inserted replaced
50990:11996ea98bbe 50991:b3c6c9ef11b8
   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