changeset 66453 | cc19f7ca2ed6 |
parent 63411 | e051eea34990 |
child 67929 | 30486b96274d |
66452:450cefec7c11 | 66453:cc19f7ca2ed6 |
---|---|
2 |
2 |
3 section \<open>Unbalanced Tree Implementation of Set\<close> |
3 section \<open>Unbalanced Tree Implementation of Set\<close> |
4 |
4 |
5 theory Tree_Set |
5 theory Tree_Set |
6 imports |
6 imports |
7 "~~/src/HOL/Library/Tree" |
7 "HOL-Library.Tree" |
8 Cmp |
8 Cmp |
9 Set_by_Ordered |
9 Set_by_Ordered |
10 begin |
10 begin |
11 |
11 |
12 fun isin :: "'a::linorder tree \<Rightarrow> 'a \<Rightarrow> bool" where |
12 fun isin :: "'a::linorder tree \<Rightarrow> 'a \<Rightarrow> bool" where |