src/HOL/Library/RBT_Impl.thy
2015-11-05 wenzelm 2015-11-05 isabelle update_cartouches -c -t;
2015-10-17 haftmann 2015-10-17 qualify some names stemming from internal bootstrap constructions
2015-09-22 nipkow 2015-09-22 tuned references
2015-09-06 wenzelm 2015-09-06 do not expose low-level "_def" facts of 'function' definitions, to avoid potential confusion with the situation of plain 'definition';
2015-09-01 wenzelm 2015-09-01 eliminated \<Colon>;
2015-06-17 wenzelm 2015-06-17 isabelle update_cartouches;
2015-03-03 blanchet 2015-03-03 removed needless (and inconsistent) qualifier that messes up with Mirabelle
2015-02-18 haftmann 2015-02-18 inlined rules to free user-space from technical names
2014-11-02 wenzelm 2014-11-02 modernized header;
2014-09-11 blanchet 2014-09-11 updated news
2014-09-09 blanchet 2014-09-09 half-ported Imperative HOL to new datatypes
2014-09-09 blanchet 2014-09-09 use 'datatype_new' (soon to be renamed 'datatype') in Isabelle's libraries
2014-08-18 blanchet 2014-08-18 reordered some (co)datatype property names for more consistency
2014-07-04 haftmann 2014-07-04 reduced name variants for assoc and commute on plus and mult
2014-02-21 blanchet 2014-02-21 adapted to renaming of datatype 'cases' and 'recs' to 'case' and 'rec'
2014-02-14 blanchet 2014-02-14 merged 'Option.map' and 'Option.map_option'
2014-02-12 blanchet 2014-02-12 adapted to 'xxx_{case,rec}' renaming, to new theorem names, and to new variable names in theorems * * * more transition of 'xxx_rec' to 'rec_xxx' and same for case * * * compile * * * 'rename_tac's to avoid referring to generated names * * * more robust scripts with 'rename_tac' * * * 'where' -> 'of' * * * 'where' -> 'of' * * * renamed 'xxx_rec' to 'rec_xxx'
2014-02-12 blanchet 2014-02-12 renamed '{prod,sum,bool,unit}_case' to 'case_...'
2014-02-12 blanchet 2014-02-12 avoid old 'prod.simps' -- better be more specific
2013-09-03 wenzelm 2013-09-03 tuned proofs -- clarified flow of facts wrt. calculation;
2012-10-10 Andreas Lochbihler 2012-10-10 fix code equation for RBT_Impl.fold
2012-10-10 Andreas Lochbihler 2012-10-10 correct definition for skip_black
2012-10-10 Andreas Lochbihler 2012-10-10 efficient construction of red black trees from sorted associative lists
2012-09-20 Andreas Lochbihler 2012-09-20 more efficient code setup
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