11 

    11 

    12 \definecolor{darkblue}{rgb}{0,0,0.6}

    12 \definecolor{darkblue}{rgb}{0,0,0.6}

    13 \hypersetup{colorlinks=true}

    13 \hypersetup{colorlinks=true}

    14 \hypersetup{linkcolor=darkblue}

    14 \hypersetup{linkcolor=darkblue}

    15 \hypersetup{urlcolor=darkblue}

    15 \hypersetup{urlcolor=darkblue}

    18 

    16 

    19 \newcommand{\tttext}[1]{{\consolas{#1}}}

    17 \newcommand{\tttext}[1]{{\consolas{#1}}}

    20 

    18 

    21 \newcommand{\dn}{\stackrel{\mbox{\scriptsize def}}{=}}%

    19 \newcommand{\dn}{\stackrel{\mbox{\scriptsize def}}{=}}%

    22 \newcommand{\slidecaption}{}

    20 \newcommand{\slidecaption}{}