equal
deleted
inserted
replaced
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 |> Simplifier.add_simps (@{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 |
30 {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 |