1(* 2 * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230) 3 * 4 * SPDX-License-Identifier: BSD-2-Clause 5 *) 6 7signature METHOD_EXTRAS = 8sig 9 (* `then_all_new m1 m2` is equivalent to `(m1; m2)`. *) 10 val then_all_new: 11 (Proof.context -> Method.method) * (Proof.context -> Method.method) 12 -> Proof.context -> Method.method; 13end 14 15structure MethodExtras: METHOD_EXTRAS = 16struct 17open Method 18 19fun then_all_new (m1, m2) = 20 Combinator (no_combinator_info, Then_All_New, [Basic m1, Basic m2]) |> evaluate 21 22end 23