Isabelle/ML is a strange programming environment for writing code that can also interact with Isabelle theories. The basic example of this is the idea of antiquotations (a kind of preprocessor) that allows referring to terms defined in theories.

In the following snippet the command ML_val inteprets the text as a Isabelle/ML program. The only interesting detail here is that the @{term "HOL.conj"} is an antiquotation and is substituted by the value Const ("HOL.conj", "bool => bool => bool") before the expression is evaluated.

ML_val  ‹
  @{term HOL.conj}
› (* val it = Const ("HOL.conj", "bool => bool => bool") : term *)

Antiquotations are more than a syntactic convenience that is expanded by the preprocessor. They are typed, and most importantly, programmable. Because they are typed, many basic errors in Isabelle/ML programs are caught by the type-checker. You cannot refer to a theorem and get a term instead. Because they are programmable, they can pperform basic validation and report errors.

This is convenient because it prevents other simple mistakes. For example, in the following snippet, the typo HOL.cojn is found immediately but the equivalent construction passes silently.

ML_val  ‹@{term HOL.cojn}›  (* Undefined constant: "HOL.cojn" *)
ML_val  ‹
  Const ("HOL.cojn", dummyT)
> (* val it = Const ("HOL.cojn", "_") : term *)