src/HOL/Library/RBT_Impl.thy
2012-07-31 kuncar 2012-07-31 a couple of additions to RBT formalization to allow us to implement RBT_Set
2012-04-13 wenzelm 2012-04-13 updated headers;
2012-04-13 Andreas Lochbihler 2012-04-13 move RBT implementation into type class contexts
2012-04-06 haftmann 2012-04-06 no preference wrt. fold(l/r); prefer fold rather than foldr for iterating over lists in generated code
2012-01-06 haftmann 2012-01-06 incorporated canonical fold combinator on lists into body of List theory; refactored passages on List.fold(l/r)
2011-12-26 haftmann 2011-12-26 incorporated More_Set and More_List into the Main body -- to be consolidated later
2011-03-13 wenzelm 2011-03-13 tuned headers;
2010-12-08 haftmann 2010-12-08 hide popular names R and B
2010-09-13 nipkow 2010-09-13 renamed lemmas: ext_iff -> fun_eq_iff, set_ext_iff -> set_eq_iff, set_ext -> set_eqI
2010-09-07 nipkow 2010-09-07 expand_fun_eq -> ext_iff expand_set_eq -> set_ext_iff Naming in line now with multisets
2010-06-28 haftmann 2010-06-28 merged constants "split" and "prod_case"
2010-06-18 haftmann 2010-06-18 prefer fold over foldl
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