| changeset 66453 | cc19f7ca2ed6 |
| parent 63411 | e051eea34990 |
| child 67406 | 23307fd33906 |
| 66452:450cefec7c11 | 66453:cc19f7ca2ed6 |
|---|---|
7 |
7 |
8 theory AVL_Set |
8 theory AVL_Set |
9 imports |
9 imports |
10 Cmp |
10 Cmp |
11 Isin2 |
11 Isin2 |
12 "~~/src/HOL/Number_Theory/Fib" |
12 "HOL-Number_Theory.Fib" |
13 begin |
13 begin |
14 |
14 |
15 type_synonym 'a avl_tree = "('a,nat) tree" |
15 type_synonym 'a avl_tree = "('a,nat) tree" |
16 |
16 |
17 text {* Invariant: *} |
17 text {* Invariant: *} |