equal
deleted
inserted
replaced
6 imports |
6 imports |
7 Tree234 |
7 Tree234 |
8 Cmp |
8 Cmp |
9 Set_Specs |
9 Set_Specs |
10 begin |
10 begin |
|
11 |
|
12 declare sorted_wrt.simps(2)[simp del] |
11 |
13 |
12 subsection \<open>Set operations on 2-3-4 trees\<close> |
14 subsection \<open>Set operations on 2-3-4 trees\<close> |
13 |
15 |
14 fun isin :: "'a::linorder tree234 \<Rightarrow> 'a \<Rightarrow> bool" where |
16 fun isin :: "'a::linorder tree234 \<Rightarrow> 'a \<Rightarrow> bool" where |
15 "isin Leaf x = False" | |
17 "isin Leaf x = False" | |