diff -r e60333aa18ca -r aece5cc9efb7 src/Doc/Nitpick/document/root.tex --- a/src/Doc/Nitpick/document/root.tex Tue Apr 20 22:53:24 2021 +0200 +++ b/src/Doc/Nitpick/document/root.tex Thu Apr 22 10:11:11 2021 +0200 @@ -2,7 +2,6 @@ \usepackage[T1]{fontenc} \usepackage{amsmath} \usepackage{amssymb} -\usepackage[english]{babel} \usepackage{color} \usepackage{footmisc} \usepackage{graphicx} @@ -32,7 +31,7 @@ \def\undef{(\lambda x.\; \_)} %\def\unr{\textit{others}} \def\unr{\ldots} -\def\Abs#1{\hbox{\rm{\flqq}}{\,#1\,}\hbox{\rm{\frqq}}} +\def\Abs#1{\hbox{\rm{\guillemetleft}}{\,#1\,}\hbox{\rm{\guillemetright}}} \def\Q{{\smash{\lower.2ex\hbox{$\scriptstyle?$}}}} \hyphenation{Mini-Sat size-change First-Steps grand-parent nit-pick