diff options
Diffstat (limited to 'doc/common/macros.tex')
| -rwxr-xr-x | doc/common/macros.tex | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/doc/common/macros.tex b/doc/common/macros.tex index 3fe782d905..418fe1436e 100755 --- a/doc/common/macros.tex +++ b/doc/common/macros.tex @@ -202,6 +202,7 @@ \newcommand{\str}{\textrm{\textsl{string}}} \newcommand{\subsequentletter}{\textrm{\textsl{subsequent\_letter}}} \newcommand{\switch}{\textrm{\textsl{switch}}} +\newcommand{\messagetoken}{\textrm{\textsl{message\_token}}} \newcommand{\tac}{\textrm{\textsl{tactic}}} \newcommand{\terms}{\textrm{\textsl{terms}}} \newcommand{\term}{\textrm{\textsl{term}}} |