diff -r 9ce78065f68d -r 2f5a4d76756d style.sty --- a/style.sty Fri Oct 25 17:23:23 2019 +0100 +++ b/style.sty Sun Oct 27 11:16:09 2019 +0000 @@ -14,10 +14,13 @@ \newcommand{\ZERO}{\mbox{\bf 0}} \newcommand{\ONE}{\mbox{\bf 1}} \newcommand{\Left}{\textit{Left}} +\newcommand{\Right}{\textit{Right}} \newcommand{\Der}{\textit{Der}} \newcommand{\der}{\textit{der}} \newcommand{\Ders}{\textit{Ders}} \newcommand{\ders}{\textit{ders}} +\newcommand{\inj}{\textit{inj}} +\newcommand{\nullable}{\textit{nullable}} %%% for trees %% http://anorien.csc.warwick.ac.uk/mirrors/CTAN/graphics/pgf/contrib/forest/forest.pdf