diff -r 5c96fe5306a7 -r 57182b36ec01 thys2/Paper/document/root.tex
--- a/thys2/Paper/document/root.tex	Sat Feb 05 18:24:37 2022 +0000
+++ b/thys2/Paper/document/root.tex	Sun Feb 06 00:02:04 2022 +0000
@@ -34,6 +34,23 @@
 \renewcommand{\isasymin}{\ensuremath{\,\in\,}}
 
 
+\def\lexer{\mathit{lexer}}
+\def\mkeps{\mathit{mkeps}}
+\def\inj{\mathit{inj}}
+\def\Empty{\mathit{Empty}}
+\def\Left{\mathit{Left}}
+\def\Right{\mathit{Right}}
+\def\Stars{\mathit{Stars}}
+\def\Char{\mathit{Char}}
+\def\Seq{\mathit{Seq}}
+\def\Der{\mathit{Der}}
+\def\nullable{\mathit{nullable}}
+\def\Z{\mathit{Z}}
+\def\S{\mathit{S}}
+\newcommand{\ZERO}{\mbox{\bf 0}}
+\newcommand{\ONE}{\mbox{\bf 1}}
+
+
 \def\Brz{Brzozowski}
 \def\der{\backslash}
 \newtheorem{falsehood}{Falsehood}