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