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