changeset 67965 | aaa31cd0caef |
parent 67964 | 08cc5ab18c84 |
child 67967 | 5a4280946a25 |
67964:08cc5ab18c84 | 67965:aaa31cd0caef |
---|---|
4 |
4 |
5 theory Isin2 |
5 theory Isin2 |
6 imports |
6 imports |
7 Tree2 |
7 Tree2 |
8 Cmp |
8 Cmp |
9 Set_Interfaces |
9 Set_Specs |
10 begin |
10 begin |
11 |
11 |
12 fun isin :: "('a::linorder,'b) tree \<Rightarrow> 'a \<Rightarrow> bool" where |
12 fun isin :: "('a::linorder,'b) tree \<Rightarrow> 'a \<Rightarrow> bool" where |
13 "isin Leaf x = False" | |
13 "isin Leaf x = False" | |
14 "isin (Node _ l a r) x = |
14 "isin (Node _ l a r) x = |