Theory AutoCorres2.MkTermAntiquote

(*
 * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
 *
 * SPDX-License-Identifier: BSD-2-Clause
 *)

chapter "ML Antiquotations"

section "Building terms: ‹mk_term›"

theory MkTermAntiquote
imports
  Pure
begin
text ‹
  ‹mk_term›: ML antiquotation for building and splicing terms.

  See 🗏‹MkTermAntiquote_Tests.thy› for examples and tests.
›

(* Simple wrapper theory for historical reasons. *)
ML_file "mkterm_antiquote.ML"

end