diff --git a/docs/logic.tex b/docs/logic.tex
index 51b4d0290a22c785c871f7baf6de53b40cb6791a..ecebd3f4ba04ae8037fac889768530bb9da2e4d0 100644
--- a/docs/logic.tex
+++ b/docs/logic.tex
@@ -93,13 +93,13 @@ Elements of $\SigAx$ are ranged over by $\sigax$.
 Iris syntax is built up from a signature $\Sig$ and a countably infinite set $\textdom{Var}$ of variables (ranged over by metavariables $x$, $y$, $z$):
 
 \begin{align*}
-  \type ::={}&
+  \type \bnfdef{}&
       \sigtype \mid
       1 \mid
       \type \times \type \mid
       \type \to \type
 \\[0.4em]
-  \term, \prop, \pred ::={}&
+  \term, \prop, \pred \bnfdef{}&
       \var \mid
       \sigfn(\term_1, \dots, \term_n) \mid
       () \mid