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