| changeset 67964 | 08cc5ab18c84 |
| parent 67929 | 30486b96274d |
| child 67965 | aaa31cd0caef |
| 67963:9541f2c5ce8d | 67964:08cc5ab18c84 |
|---|---|
4 |
4 |
5 theory Tree234_Set |
5 theory Tree234_Set |
6 imports |
6 imports |
7 Tree234 |
7 Tree234 |
8 Cmp |
8 Cmp |
9 "../Data_Structures/Set_by_Ordered" |
9 "Set_Interfaces" |
10 begin |
10 begin |
11 |
11 |
12 subsection \<open>Set operations on 2-3-4 trees\<close> |
12 subsection \<open>Set operations on 2-3-4 trees\<close> |
13 |
13 |
14 fun isin :: "'a::linorder tree234 \<Rightarrow> 'a \<Rightarrow> bool" where |
14 fun isin :: "'a::linorder tree234 \<Rightarrow> 'a \<Rightarrow> bool" where |