| changeset 47455 | 26315a545e26 |
| parent 47450 | 2ada2be850cb |
| child 48621 | 877df57629e3 |
| 47454:479b4d6b9562 | 47455:26315a545e26 |
|---|---|
1 (* Title: RBT_Impl.thy |
1 (* Title: HOL/Library/RBT_Impl.thy |
2 Author: Markus Reiter, TU Muenchen |
2 Author: Markus Reiter, TU Muenchen |
3 Author: Alexander Krauss, TU Muenchen |
3 Author: Alexander Krauss, TU Muenchen |
4 *) |
4 *) |
5 |
5 |
6 header {* Implementation of Red-Black Trees *} |
6 header {* Implementation of Red-Black Trees *} |