diff --git a/formalism/marked.tex b/formalism/marked.tex
index ab49b24..cdacfb5 100644
--- a/formalism/marked.tex
+++ b/formalism/marked.tex
@@ -13,6 +13,11 @@ \section{Marked lambda calculus}
 numbers, booleans, and product types. Typed holes (written $\EEHole$) are included to model
 incomplete editor states \`a la Hazelnut but are not essential.
 
+\begin{mechanization}
+  \item core.agda
+  \item marking.agda
+\end{mechanization}
+
 \subsection{Syntax}
 \label{sec:marked-syntax}
 \[\begin{array}{rrcl}
diff --git a/formalism/patterned.tex b/formalism/patterned.tex
index 28605a7..d712db8 100644
--- a/formalism/patterned.tex
+++ b/formalism/patterned.tex
@@ -9,6 +9,8 @@
 \section{Extension: patterned let expressions}
 \label{sec:patterned}
 
+\nomechanization{}
+
 \subsection{Syntax}
 \label{sec:patterned-syntax}
 \[\begin{array}{rrcl}
diff --git a/formalism/polymorphism.tex b/formalism/polymorphism.tex
index bae57c3..fc00367 100644
--- a/formalism/polymorphism.tex
+++ b/formalism/polymorphism.tex
@@ -16,6 +16,8 @@ \section{Extension: System F-style polymorphism}
 (alongside extensions of the original consistency, etc. judgments) and linked by a marking
 operation.
 
+\nomechanization{}
+
 \subsection{Syntax}
 \label{sec:polymorphism-syntax}
 The syntax of unmarked types is exactly that of the original types alongside additional forms for
diff --git a/formalism/preamble/preamble.tex b/formalism/preamble/preamble.tex
index 01afe38..9420c87 100644
--- a/formalism/preamble/preamble.tex
+++ b/formalism/preamble/preamble.tex
@@ -18,6 +18,7 @@
 
 % font
 \usepackage{iftex}
+\usepackage{fontspec}
 \ifPDFTeX
   \usepackage{libertinust1math}
   \usepackage{libertine}
@@ -32,6 +33,9 @@
 \usepackage{relsize}
 \usepackage{centernot}
 
+% no indentation
+\usepackage{parskip}
+
 % hyperlinks
 \usepackage[colorlinks=true, linkcolor=purple]{hyperref}
 \usepackage[capitalise, noabbrev]{cleveref}
@@ -60,3 +64,15 @@
 
 % utilities
 \input{preamble/utilities}
+
+% mechanization notices
+\newenvironment{mechanization}{
+  \textsc{Mechanization} $\bm{\bigcirc}$
+  %
+  \begin{itemize}[label=$\blacktriangleright$, noitemsep]
+    \ttfamily
+}{
+  \end{itemize}
+}
+
+\newcommand{\nomechanization}{\textsc{Mechanization} $\times$}
diff --git a/formalism/typed.tex b/formalism/typed.tex
index d4596e3..ec5f84b 100644
--- a/formalism/typed.tex
+++ b/formalism/typed.tex
@@ -10,6 +10,8 @@
 \section{Typed hazelnut}
 \label{sec:typed}
 
+\nomechanization{}
+
 \subsection{Syntax}
 \label{sec:typed-syntax}
 Zippered types are the same as in the untyped model.
diff --git a/formalism/untyped.tex b/formalism/untyped.tex
index cd5822e..fe9b6d6 100644
--- a/formalism/untyped.tex
+++ b/formalism/untyped.tex
@@ -8,6 +8,10 @@
 \section{Untyped hazelnut}
 \label{sec:untyped}
 
+\begin{mechanization}
+  \item hazelnut.agda
+\end{mechanization}
+
 \subsection{Syntax}
 \label{sec:untyped-syntax}
 \[\begin{array}{rrcl}