| #
97bce028 |
|
13-Jun-2018 |
nipkow <none@none> |
qualify interpretations to avoid clashes
|
| #
83ad70a0 |
|
12-Jun-2018 |
nipkow <none@none> |
more abstract naming
|
| #
5fde6c5f |
|
11-Jun-2018 |
nipkow <none@none> |
tuned order of arguments
|
| #
99ffcf66 |
|
07-Apr-2018 |
nipkow <none@none> |
moved and renamed lemmas
|
| #
5d7063f6 |
|
07-Apr-2018 |
nipkow <none@none> |
tuned
|
| #
3e62aabe |
|
02-Dec-2017 |
haftmann <none@none> |
more simplification rules
--HG--
extra : rebase_source : 2b7704ac9459d132ec9fea4769b865bdcad1548f
|
| #
c612034e |
|
15-Jun-2017 |
nipkow <none@none> |
tuned
|
| #
021fcf0e |
|
14-Jun-2017 |
nipkow <none@none> |
simplified delete/proof
|
| #
02fbd8bb |
|
28-Jan-2017 |
nipkow <none@none> |
split balance into two, clearer etc
|
| #
9fb150c2 |
|
27-Jan-2017 |
nipkow <none@none> |
tuned name
|
| #
05211681 |
|
27-Jan-2017 |
nipkow <none@none> |
removed unclear clause; slower but clearer
|
| #
bf21c69e |
|
26-Jan-2017 |
nipkow <none@none> |
removed contribution by Daniel Stuewe, too detailed.
|
| #
ac866971 |
|
26-Jan-2017 |
nipkow <none@none> |
added concise log height bound lemma
|
| #
70a0e3ef |
|
25-Jan-2017 |
nipkow <none@none> |
tuned
|
| #
54a0a039 |
|
16-Oct-2016 |
haftmann <none@none> |
more standardized theorem names for facts involving the div and mod identity
|
| #
4fd0cb28 |
|
07-Jul-2016 |
nipkow <none@none> |
got rid of class cmp; added height-size proofs by Daniel Stuewe
|
| #
315f2fe3 |
|
06-Mar-2016 |
nipkow <none@none> |
tuned
|
| #
f8ccebe2 |
|
29-Nov-2015 |
nipkow <none@none> |
RBT invariants for insert
|
| #
a82524e6 |
|
27-Nov-2015 |
nipkow <none@none> |
paint root black after insert and delete
|
| #
1964277f |
|
14-Nov-2015 |
nipkow <none@none> |
tuned white space
|
| #
16e9bbf5 |
|
05-Nov-2015 |
nipkow <none@none> |
tuned
|
| #
efd623c1 |
|
05-Nov-2015 |
nipkow <none@none> |
Convertd to 3-way comparisons
|
| #
1bc192be |
|
13-Oct-2015 |
nipkow <none@none> |
added invar empty
|
| #
72b4772b |
|
23-Sep-2015 |
nipkow <none@none> |
tuned
|
| #
6fc2a136 |
|
22-Sep-2015 |
nipkow <none@none> |
added red black trees
--HG--
extra : rebase_source : 28e43c87d5eb14090fa401987d8131c2067f6ab7
|