Fix typos in catch validation

Author: rossberg

document/core/valid/instructions.rst

@@ -1972,7 +1972,7 @@ Control Instructions
 
 * The tag :math:`C.\CTAGS[x]` must be defined in the context.
 
-* Let :math:`[t^\ast] \to [{t'}^\ast]` be the :ref:`tag type <syntax-tagtype>` :math:`C.\CTAGS[x]`.
+* Let :math:`[t^\ast] \to [{t'}^\ast]` be the :ref:`expansion <aux-expand-deftype>` of the :ref:`tag type <syntax-tagtype>` :math:`C.\CTAGS[x]`.
 
 * The :ref:`result type <syntax-resulttype>` :math:`[{t'}^\ast]` must be empty.
 
@@ -1984,7 +1984,7 @@ Control Instructions
 
 .. math::
    \frac{
-     C.\CTAGS[x] = [t^\ast] \toF []
+     \expanddt(C.\CTAGS[x]) = [t^\ast] \toF []
      \qquad
      C.\CLABELS[l] = [t^\ast]
    }{
@@ -1996,21 +1996,21 @@ Control Instructions
 
 * The tag :math:`C.\CTAGS[x]` must be defined in the context.
 
-* Let :math:`[t^\ast] \to [{t'}^\ast]` be the :ref:`tag type <syntax-tagtype>` :math:`C.\CTAGS[x]`.
+* Let :math:`[t^\ast] \to [{t'}^\ast]` be the :ref:`expansion <aux-expand-deftype>` of the :ref:`tag type <syntax-tagtype>` :math:`C.\CTAGS[x]`.
 
 * The :ref:`result type <syntax-resulttype>` :math:`[{t'}^\ast]` must be empty.
 
 * The label :math:`C.\CLABELS[l]` must be defined in the context.
 
-* The :ref:`result type <syntax-resulttype>` :math:`[t^\ast]` must be the same as :math:`C.\CLABELS[l]` with |EXNREF| appended.
+* The :ref:`result type <syntax-resulttype>` :math:`[t^\ast~(\REF~\EXN)]` must :ref:`match <match-resulttype>` :math:`C.\CLABELS[l]`.
 
 * Then the catch clause is valid.
 
 .. math::
    \frac{
-     C.\CTAGS[x] = [t^\ast] \toF []
+     \expanddt(C.\CTAGS[x]) = [t^\ast] \toF []
      \qquad
-     C.\CLABELS[l] = [t^\ast~\EXNREF]
+     C \vdashresulttypematch [t^\ast~(\REF~\EXN)] \matchesresulttype C.\CLABELS[l]
    }{
      C \vdashcatch \CATCHREF~x~l \ok
    }
@@ -2036,13 +2036,13 @@ Control Instructions
 
 * The label :math:`C.\CLABELS[l]` must be defined in the context.
 
-* The :ref:`result type <syntax-resulttype>` :math:`C.\CLABELS[l] must be :math:`[\EXNREF]`.
+* The :ref:`result type <syntax-resulttype>` :math:`[(\REF~\EXN)]` must :ref:`match <match-resulttype>` :math:`C.\CLABELS[l]`.
 
 * Then the catch clause is valid.
 
 .. math::
    \frac{
-     C.\CLABELS[l] = [\EXNREF]
+     C \vdashresulttypematch [(\REF~\EXN)] \matchesresulttype C.\CLABELS[l]
    }{
      C \vdashcatch \CATCHALLREF~l \ok
    }