| changeset 48625 | 77c416ef06fa |
| parent 48624 | 9b71daba4ec7 |
| child 48627 | 3ef76d545aaf |
| 48624:9b71daba4ec7 | 48625:77c416ef06fa |
|---|---|
1 (* Title: HOL/Quotient_Examples/Lift_RBT.thy |
|
2 Author: Lukas Bulwahn and Ondrej Kuncar |
|
3 *) |
|
4 |
|
5 header {* Lifting operations of RBT trees *} |
|
6 |
|
7 theory Lift_RBT |
|
8 imports Main "~~/src/HOL/Library/RBT_Impl" |
|
9 begin |
|
10 |
|
11 (* Moved to ~~/HOL/Library/RBT" *) |
|
12 |
|
13 end |