equal
deleted
inserted
replaced
19 structure SumTree: SUM_TREE = |
19 structure SumTree: SUM_TREE = |
20 struct |
20 struct |
21 |
21 |
22 (* Theory dependencies *) |
22 (* Theory dependencies *) |
23 val sumcase_split_ss = |
23 val sumcase_split_ss = |
24 HOL_basic_ss addsimps (@{thm Product_Type.split} :: @{thms sum.cases}) |
24 simpset_of (put_simpset HOL_basic_ss @{context} |
|
25 addsimps (@{thm Product_Type.split} :: @{thms sum.cases})) |
25 |
26 |
26 (* top-down access in balanced tree *) |
27 (* top-down access in balanced tree *) |
27 fun access_top_down {left, right, init} len i = |
28 fun access_top_down {left, right, init} len i = |
28 Balanced_Tree.access |
29 Balanced_Tree.access |
29 {left = (fn f => f o left), right = (fn f => f o right), init = I} len i init |
30 {left = (fn f => f o left), right = (fn f => f o right), init = I} len i init |