equal
deleted
inserted
replaced
19 structure Sum_Tree: SUM_TREE = |
19 structure Sum_Tree: 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 simpset_of (put_simpset HOL_basic_ss @{context} |
24 simpset_of (put_simpset HOL_basic_ss \<^context> |
25 addsimps (@{thm Product_Type.split} :: @{thms sum.case})) |
25 addsimps (@{thm Product_Type.split} :: @{thms sum.case})) |
26 |
26 |
27 (* top-down access in balanced tree *) |
27 (* top-down access in balanced tree *) |
28 fun access_top_down {left, right, init} len i = |
28 fun access_top_down {left, right, init} len i = |
29 Balanced_Tree.access |
29 Balanced_Tree.access |