src/HOL/Data_Structures/RBT_Set.thy
10 months ago nipkow 2018-06-13 qualify interpretations to avoid clashes
10 months ago nipkow 2018-06-12 more abstract naming
10 months ago nipkow 2018-06-11 tuned order of arguments
12 months ago nipkow 2018-04-08 moved and renamed lemmas
12 months ago nipkow 2018-04-07 tuned
16 months ago haftmann 2017-12-02 more simplification rules
22 months ago nipkow 2017-06-15 tuned
22 months ago nipkow 2017-06-14 simplified delete/proof
2017-01-28 nipkow 2017-01-28 split balance into two, clearer etc
2017-01-27 nipkow 2017-01-27 tuned name
2017-01-27 nipkow 2017-01-27 removed unclear clause; slower but clearer
2017-01-27 nipkow 2017-01-27 removed contribution by Daniel Stuewe, too detailed.
2017-01-26 nipkow 2017-01-26 added concise log height bound lemma
2017-01-25 nipkow 2017-01-25 tuned
2016-10-16 haftmann 2016-10-16 more standardized theorem names for facts involving the div and mod identity
2016-07-07 nipkow 2016-07-07 got rid of class cmp; added height-size proofs by Daniel Stuewe
2016-03-06 nipkow 2016-03-06 tuned
2015-11-29 nipkow 2015-11-29 RBT invariants for insert
2015-11-27 nipkow 2015-11-27 paint root black after insert and delete
2015-11-15 nipkow 2015-11-15 tuned white space
2015-11-05 nipkow 2015-11-05 tuned
2015-11-05 nipkow 2015-11-05 Convertd to 3-way comparisons
2015-10-13 nipkow 2015-10-13 added invar empty
2015-09-23 nipkow 2015-09-23 tuned
2015-09-22 nipkow 2015-09-22 added red black trees