changeset 67964 | 08cc5ab18c84 |
parent 67929 | 30486b96274d |
child 67965 | aaa31cd0caef |
67963:9541f2c5ce8d | 67964:08cc5ab18c84 |
---|---|
4 |
4 |
5 theory Tree23_Set |
5 theory Tree23_Set |
6 imports |
6 imports |
7 Tree23 |
7 Tree23 |
8 Cmp |
8 Cmp |
9 Set_by_Ordered |
9 Set_Interfaces |
10 begin |
10 begin |
11 |
11 |
12 fun isin :: "'a::linorder tree23 \<Rightarrow> 'a \<Rightarrow> bool" where |
12 fun isin :: "'a::linorder tree23 \<Rightarrow> 'a \<Rightarrow> bool" where |
13 "isin Leaf x = False" | |
13 "isin Leaf x = False" | |
14 "isin (Node2 l a r) x = |
14 "isin (Node2 l a r) x = |