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