src/HOL/Library/RBT.thy
2016-06-02 Manuel Eberl 2016-06-02 Hid RBT.filter
2016-05-31 eberlm 2016-05-31 Added code generation for PMFs
2015-09-24 wenzelm 2015-09-24 explicit indication of overloaded typedefs;
2015-09-01 wenzelm 2015-09-01 eliminated \<Colon>;
2015-06-17 wenzelm 2015-06-17 isabelle update_cartouches;
2014-11-02 wenzelm 2014-11-02 modernized header;
2014-03-10 kuncar 2014-03-10 hide implementation details
2014-02-18 kuncar 2014-02-18 simplify proofs because of the stronger reflexivity prover
2014-02-14 blanchet 2014-02-14 merged 'Option.map' and 'Option.map_option'
2014-02-12 blanchet 2014-02-12 renamed '{prod,sum,bool,unit}_case' to 'case_...'
2013-08-13 kuncar 2013-08-13 remove unnecessary dependencies on Library/Quotient_*
2013-03-08 kuncar 2013-03-08 patch Isabelle ditribution to conform to changes regarding the parametricity
2012-10-19 kuncar 2012-10-19 don't include Quotient_Option - workaround to a transfer bug
2012-10-18 kuncar 2012-10-18 new theorem
2012-10-12 wenzelm 2012-10-12 discontinued obsolete typedef (open) syntax;
2012-07-31 kuncar 2012-07-31 use lifting/transfer formalization of RBT from Lift_RBT
2012-04-13 Andreas Lochbihler 2012-04-13 move RBT implementation into type class contexts
2012-02-21 bulwahn 2012-02-21 subtype preprocessing in Quickcheck; adding option use_subtype; tuned
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-20 bulwahn 2011-12-20 adding quickcheck generators in some HOL-Library theories
2011-11-30 wenzelm 2011-11-30 prefer typedef without extra definition and alternative name; tuned proofs;
2011-06-01 bulwahn 2011-06-01 splitting RBT theory into RBT and RBT_Mapping
2010-11-18 haftmann 2010-11-18 proper qualification needed due to shadowing on theory merge
2010-09-13 haftmann 2010-09-13 established emerging canonical names *_eqI and *_eq_iff
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-08-27 haftmann 2010-08-27 renamed class/constant eq to equal; tuned some instantiations
2010-06-18 haftmann 2010-06-18 prefer fold over foldl
2010-05-21 haftmann 2010-05-21 tuned
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.