1(*
2 * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
3 *
4 * SPDX-License-Identifier: BSD-2-Clause
5 *)
6
7text \<open>
8  mk_term: ML antiquotation for building and splicing terms.
9
10  See MkTermAntiquote_Tests for examples and tests.
11\<close>
12theory MkTermAntiquote
13imports
14  Pure
15begin
16
17(* Simple wrapper theory for historical reasons. *)
18ML_file "mkterm_antiquote.ML"
19
20end