diff --git a/document/legacy/exceptions/exec.rst b/document/legacy/exceptions/exec.rst
index e2c9b239..15d30b1b 100644
--- a/document/legacy/exceptions/exec.rst
+++ b/document/legacy/exceptions/exec.rst
@@ -126,7 +126,7 @@ Control Instructions
    \begin{array}{l}
    F; \val^m~(\TRY~\X{bt}~\instr_1^\ast~(\CATCH~x~\instr_2^\ast)^\ast~(\CATCHALL~\instr_3^\ast)^?~\END
    \quad \stepto \\
-   \qquad F; \LABEL_n\{\epsilon\}~(\HANDLER_n\{(\CATCH~a_x~\instr_2^\ast)^\ast~(\CATCHALL~\instr_3^\ast)^?\}~\val^m~\instr_1^\ast~\END)~\END \\
+   \qquad F; \LABEL_n\{\epsilon\}~(\HANDLER_n\{(\CATCH~a_x~\instr_2^\ast)^\ast~(\CATCHALL~\instr_3^\ast)^?\}~\val^m~\instr_1^\ast~\END)~\END \\ \qquad
    (\iff \expand_F(\X{bt}) = [t_1^m] \to [t_2^n] \land (F.\AMODULE.\MITAGS[x]=a_x)^\ast)
    \end{array}
 
diff --git a/document/legacy/exceptions/valid.rst b/document/legacy/exceptions/valid.rst
index 03f337d5..8a13ee93 100644
--- a/document/legacy/exceptions/valid.rst
+++ b/document/legacy/exceptions/valid.rst
@@ -27,7 +27,7 @@ Existing typing rules are adjusted as follows:
 
 * All rules that extend the context with new labels use an absent |LCATCH| flag.
 
-* All rules that inspect the context for a label ignore the presence of an |LCATCH| flag.
+* All rules that inspect the context for a label ignore the presence of a |LCATCH| flag.
 
 .. note::
    This flag is used to distinguish labels bound by catch clauses, which can be targeted by |RETHROW|.
@@ -74,6 +74,7 @@ Control Instructions
 * Then the compound instruction is valid with type :math:`[t_1^\ast] \to [t_2^\ast]`.
 
 .. math::
+   ~\\
    \frac{
    \begin{array}{c}
      C \vdashblocktype \blocktype : [t_1^\ast] \to [t_2^\ast]
@@ -89,7 +90,7 @@ Control Instructions
 
 
 .. note::
-   The :ref:`notation <notation-extend>` :math:`C,\CLABELS\,(\LCATCH^?~[t^\ast])` inserts the new label type at index :math:`0`, shifting all others.
+   The :ref:`notation <notation-extend>` :math:`C,\CLABELS\,(\LCATCH~[t^\ast])` inserts the new label type at index :math:`0`, shifting all others.
 
 
 .. _valid-try-delegate:
@@ -109,6 +110,7 @@ Control Instructions
 * Then the compound instruction is valid with type :math:`[t_1^\ast] \to [t_2^\ast]`.
 
 .. math::
+   ~\\
    \frac{
      C \vdashblocktype \blocktype : [t_1^\ast] \to [t_2^\ast]
      \qquad
@@ -138,6 +140,7 @@ Control Instructions
 
 
 .. math::
+   ~\\
    \frac{
      C.\CLABELS[l] = \LCATCH~[t^\ast]
    }{