diff options
Diffstat (limited to 'doc/common')
| -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 6cbd06eae2..47409b9845 100755 --- a/doc/common/macros.tex +++ b/doc/common/macros.tex @@ -172,6 +172,7 @@ \newcommand{\localdecls}{\textrm{\textsl{local\_decls}}} \newcommand{\ident}{\textrm{\textsl{ident}}} \newcommand{\accessident}{\textrm{\textsl{access\_ident}}} +\newcommand{\possiblybracketedident}{\textrm{\textsl{possibly\_bracketed\_ident}}} \newcommand{\inductivebody}{\textrm{\textsl{ind\_body}}} \newcommand{\inductive}{\textrm{\textsl{inductive}}} \newcommand{\naturalnumber}{\textrm{\textsl{natural}}} |