equal
deleted
inserted
replaced
6 |
6 |
7 structure SumTree = |
7 structure SumTree = |
8 struct |
8 struct |
9 |
9 |
10 (* Theory dependencies *) |
10 (* Theory dependencies *) |
11 val proj_in_rules = [@{thm Projl_Inl}, @{thm Projr_Inr}] |
|
12 val sumcase_split_ss = |
11 val sumcase_split_ss = |
13 HOL_basic_ss addsimps (@{thm Product_Type.split} :: @{thms sum.cases}) |
12 HOL_basic_ss addsimps (@{thm Product_Type.split} :: @{thms sum.cases}) |
14 |
13 |
15 (* top-down access in balanced tree *) |
14 (* top-down access in balanced tree *) |
16 fun access_top_down {left, right, init} len i = |
15 fun access_top_down {left, right, init} len i = |