src/HOL/Library/RBT_Set.thy
2016-10-17 nipkow 2016-10-17 setprod -> prod
2016-10-17 nipkow 2016-10-17 setsum -> sum
2016-08-10 wenzelm 2016-08-10 tuned proofs;
2016-05-31 eberlm 2016-05-31 Added code generation for PMFs
2015-09-01 wenzelm 2015-09-01 eliminated \<Colon>;
2015-07-06 wenzelm 2015-07-06 tuned proofs;
2015-06-25 wenzelm 2015-06-25 tuned proofs;
2015-06-17 wenzelm 2015-06-17 isabelle update_cartouches;
2014-11-02 wenzelm 2014-11-02 modernized header;
2014-09-18 haftmann 2014-09-18 product over monoids for lists
2014-09-11 blanchet 2014-09-11 fixed situation in 'primrec' whereby the original value of a constructor argument of nested type was not translated correctly to a 'map fst'
2014-08-07 blanchet 2014-08-07 no need for 'set_simps' now that 'datatype_new' generates the desired 'set' property
2014-07-05 haftmann 2014-07-05 prefer ac_simps collections over separate name bindings for add and mult
2014-04-29 wenzelm 2014-04-29 prefer plain ASCII / latex over not-so-universal Unicode;
2014-04-10 kuncar 2014-04-10 more appropriate name (Lifting.invariant -> eq_onp)
2014-03-19 haftmann 2014-03-19 elongated INFI and SUPR, to reduced risk of confusing theorems names in the future while still being consistent with INTER and UNION
2014-03-18 haftmann 2014-03-18 consolidated theorem names containing INFI and SUPR: have INF and SUP instead uniformly
2014-03-10 kuncar 2014-03-10 hide implementation details
2014-02-19 blanchet 2014-02-19 merged 'List.set' with BNF-generated 'set'
2014-02-18 kuncar 2014-02-18 simplify proofs because of the stronger reflexivity prover
2013-11-05 hoelzl 2013-11-05 move Lubs from HOL to HOL-Library (replaced by conditionally complete lattices)
2013-09-27 nipkow 2013-09-27 added Bleast code eqns for RBT
2013-09-20 Andreas Lochbihler 2013-09-20 prefer Code.abort over code_abort
2013-03-26 haftmann 2013-03-26 explicit sublocale dependency for Min/Max yields more appropriate Min/Max prefix for a couple of facts
2013-03-23 haftmann 2013-03-23 fundamental revision of big operators on sets
2013-02-14 haftmann 2013-02-14 consolidation of library theories on product orders
2013-01-15 kuncar 2013-01-15 restore code equations for List.set in RBT_Set; make Scala happy according to 7.1 in the code generator manual
2012-10-20 haftmann 2012-10-20 moved quite generic material from theory Enum to more appropriate places
2012-10-18 kuncar 2012-10-18 tuned proofs
2012-10-09 kuncar 2012-10-09 use Set.filter instead of Finite_Set.filter, which is removed then
2012-10-09 kuncar 2012-10-09 rename Set.project to Set.filter - more appropriate name
2012-07-31 kuncar 2012-07-31 implementation of sets by RBT trees for the code generator