src/HOL/Library/RBT.thy
2010-08-27 ago renamed class/constant eq to equal; tuned some instantiations
2010-06-18 ago prefer fold over foldl
2010-05-21 ago tuned
2010-05-20 ago implement Mapping.map_entry
2010-04-21 ago merged
2010-04-16 ago replaced generic 'hide' command by more conventional 'hide_class', 'hide_type', 'hide_const', 'hide_fact' -- frees some popular keywords;
2010-04-15 ago theory RBT with abstract type of red-black trees backed by implementation RBT_Impl
2010-03-06 ago some lemma refinements
2010-03-06 ago added bulkload; tuned document
2010-03-05 ago moved lemma map_sorted_distinct_set_unique
2010-03-05 ago various refinements
2010-03-03 ago restructured RBT theory
2010-03-03 ago more explicit naming scheme
2009-07-28 ago tuned
2009-07-27 ago added missing proof of RBT.map_of_alist_of (contributed by Peter Lammich)
2009-03-27 ago normalized imports
2009-03-04 ago Made Option a separate theory and renamed option_map to Option.map
2008-06-26 ago established Plain theory and image
2008-03-03 ago new theory of red-black trees, an efficient implementation of finite maps.