handouts/graphs.tex
author Christian Urban <christian.urban@kcl.ac.uk>
Wed, 01 Oct 2025 10:37:20 +0100
changeset 996 e37c4d6c08fe
parent 990 ef63ae3586b8
permissions -rw-r--r--
updated
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
497
c498cb53a9a8 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
     1
\documentclass{article}
990
ef63ae3586b8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 497
diff changeset
     2
\usepackage{tikz}
ef63ae3586b8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 497
diff changeset
     3
\usepackage{pgf}
ef63ae3586b8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 497
diff changeset
     4
\usepackage{pgfplots}
ef63ae3586b8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 497
diff changeset
     5
ef63ae3586b8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 497
diff changeset
     6
\pgfplotsset{compat=1.15}
ef63ae3586b8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 497
diff changeset
     7
ef63ae3586b8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 497
diff changeset
     8
ef63ae3586b8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 497
diff changeset
     9
%% DATA for the graphs: first x coordinate, second y coordinate
ef63ae3586b8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 497
diff changeset
    10
\begin{filecontents}{re-python2.data}
ef63ae3586b8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 497
diff changeset
    11
1 0.033
ef63ae3586b8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 497
diff changeset
    12
5 0.036
ef63ae3586b8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 497
diff changeset
    13
10 0.034
ef63ae3586b8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 497
diff changeset
    14
15 0.036
ef63ae3586b8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 497
diff changeset
    15
18 0.059
ef63ae3586b8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 497
diff changeset
    16
19 0.084
ef63ae3586b8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 497
diff changeset
    17
20 0.141
ef63ae3586b8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 497
diff changeset
    18
21 0.248
ef63ae3586b8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 497
diff changeset
    19
22 0.485
ef63ae3586b8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 497
diff changeset
    20
23 0.878
ef63ae3586b8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 497
diff changeset
    21
24 1.71
ef63ae3586b8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 497
diff changeset
    22
25 3.40
ef63ae3586b8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 497
diff changeset
    23
26 7.08
ef63ae3586b8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 497
diff changeset
    24
27 14.12
ef63ae3586b8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 497
diff changeset
    25
28 26.69
ef63ae3586b8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 497
diff changeset
    26
\end{filecontents}
ef63ae3586b8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 497
diff changeset
    27
ef63ae3586b8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 497
diff changeset
    28
\begin{filecontents}{re-java.data}
ef63ae3586b8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 497
diff changeset
    29
5  0.00298
ef63ae3586b8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 497
diff changeset
    30
10  0.00418
ef63ae3586b8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 497
diff changeset
    31
15  0.00996
ef63ae3586b8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 497
diff changeset
    32
16  0.01710
ef63ae3586b8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 497
diff changeset
    33
17  0.03492
ef63ae3586b8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 497
diff changeset
    34
18  0.03303
ef63ae3586b8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 497
diff changeset
    35
19  0.05084
ef63ae3586b8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 497
diff changeset
    36
20  0.10177
ef63ae3586b8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 497
diff changeset
    37
21  0.19960
ef63ae3586b8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 497
diff changeset
    38
22  0.41159
ef63ae3586b8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 497
diff changeset
    39
23  0.82234
ef63ae3586b8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 497
diff changeset
    40
24  1.70251
ef63ae3586b8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 497
diff changeset
    41
25  3.36112
ef63ae3586b8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 497
diff changeset
    42
26  6.63998
ef63ae3586b8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 497
diff changeset
    43
27  13.35120
ef63ae3586b8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 497
diff changeset
    44
28  29.81185
ef63ae3586b8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 497
diff changeset
    45
\end{filecontents}
ef63ae3586b8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 497
diff changeset
    46
ef63ae3586b8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 497
diff changeset
    47
\begin{filecontents}{re3a.data}
ef63ae3586b8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 497
diff changeset
    48
1 0.00003
ef63ae3586b8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 497
diff changeset
    49
500001 0.22527
ef63ae3586b8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 497
diff changeset
    50
1000001 0.62752
ef63ae3586b8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 497
diff changeset
    51
1500001 0.88485
ef63ae3586b8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 497
diff changeset
    52
2000001 1.39815
ef63ae3586b8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 497
diff changeset
    53
2500001 1.68619
ef63ae3586b8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 497
diff changeset
    54
3000001 1.94957
ef63ae3586b8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 497
diff changeset
    55
3500001 2.15878
ef63ae3586b8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 497
diff changeset
    56
4000001 2.59918
ef63ae3586b8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 497
diff changeset
    57
4500001 5.90679
ef63ae3586b8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 497
diff changeset
    58
5000001 13.11295
ef63ae3586b8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 497
diff changeset
    59
5500001 19.15376
ef63ae3586b8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 497
diff changeset
    60
6000001 40.16373
ef63ae3586b8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 497
diff changeset
    61
\end{filecontents}
ef63ae3586b8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 497
diff changeset
    62
497
c498cb53a9a8 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    63
c498cb53a9a8 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    64
c498cb53a9a8 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    65
\begin{document}
c498cb53a9a8 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    66
c498cb53a9a8 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    67
\section*{Benchmarks for $(a^*)^* b$ and $a^{?\{n\}} a^{\{n\}}$}
c498cb53a9a8 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    68
c498cb53a9a8 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    69
\mbox{}\bigskip
c498cb53a9a8 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    70
c498cb53a9a8 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    71
\begin{center}
c498cb53a9a8 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    72
$(a^*)^* \cdot b$ and strings $\underbrace{a\ldots a}_{n}$\medskip\\
c498cb53a9a8 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    73
\begin{tabular}{@{}cc@{}}
c498cb53a9a8 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    74
\raisebox{5mm}{
c498cb53a9a8 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    75
\begin{tikzpicture}
c498cb53a9a8 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    76
\begin{axis}[
c498cb53a9a8 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    77
    xlabel={$n$},
c498cb53a9a8 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    78
    x label style={at={(1.05,0.0)}},
c498cb53a9a8 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    79
    ylabel={time in secs},
c498cb53a9a8 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    80
    enlargelimits=false,
c498cb53a9a8 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    81
    xtick={0,5,...,30},
c498cb53a9a8 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    82
    xmax=33,
c498cb53a9a8 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    83
    ymax=35,
c498cb53a9a8 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    84
    ytick={0,5,...,30},
c498cb53a9a8 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    85
    scaled ticks=false,
c498cb53a9a8 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    86
    axis lines=left,
c498cb53a9a8 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    87
    width=5cm,
c498cb53a9a8 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    88
    height=5cm, 
c498cb53a9a8 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    89
    legend entries={Java, Python},  
c498cb53a9a8 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    90
    legend pos=north west,
c498cb53a9a8 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    91
    legend cell align=left]
c498cb53a9a8 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    92
\addplot[blue,mark=*, mark options={fill=white}] table {re-python2.data};
c498cb53a9a8 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    93
\addplot[cyan,mark=*, mark options={fill=white}] table {re-java.data};
c498cb53a9a8 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    94
\end{axis}
c498cb53a9a8 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    95
\end{tikzpicture}}
c498cb53a9a8 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    96
&
c498cb53a9a8 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    97
\begin{tikzpicture}
c498cb53a9a8 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    98
  \begin{axis}[
c498cb53a9a8 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    99
    xlabel={$n$},
c498cb53a9a8 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   100
    x label style={at={(1.1,0.0)}},
c498cb53a9a8 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   101
    ylabel={time in secs},
c498cb53a9a8 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   102
    enlargelimits=false,
c498cb53a9a8 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   103
    ymax=35,
c498cb53a9a8 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   104
    ytick={0,5,...,30},
c498cb53a9a8 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   105
    axis lines=left,
c498cb53a9a8 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   106
    width=6.5cm,
c498cb53a9a8 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   107
    height=5cm,
c498cb53a9a8 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   108
    legend entries={Derivative matcher},  
c498cb53a9a8 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   109
    legend pos=north east,
c498cb53a9a8 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   110
    legend cell align=left]
c498cb53a9a8 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   111
\addplot[black,mark=square*,mark options={fill=white}] table {re3a.data};
c498cb53a9a8 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   112
\end{axis}
c498cb53a9a8 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   113
\end{tikzpicture}
c498cb53a9a8 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   114
\end{tabular}
c498cb53a9a8 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   115
\end{center}\bigskip
c498cb53a9a8 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   116
c498cb53a9a8 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   117
\begin{center}
c498cb53a9a8 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   118
$a^{?\{n\}} \cdot a^{\{n\}}$ and strings $\underbrace{a\ldots a}_{n}$\medskip\\
c498cb53a9a8 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   119
\begin{tabular}{@{}cc@{}}
c498cb53a9a8 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   120
\begin{tikzpicture}
c498cb53a9a8 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   121
\begin{axis}[
c498cb53a9a8 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   122
    xlabel={$n$},
c498cb53a9a8 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   123
    x label style={at={(1.05,0.0)}},
c498cb53a9a8 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   124
    ylabel={\small time in secs},
c498cb53a9a8 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   125
    enlargelimits=false,
c498cb53a9a8 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   126
    xtick={0,5,...,30},
c498cb53a9a8 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   127
    xmax=33,
c498cb53a9a8 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   128
    ymax=35,
c498cb53a9a8 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   129
    ytick={0,5,...,30},
c498cb53a9a8 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   130
    scaled ticks=false,
c498cb53a9a8 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   131
    axis lines=left,
c498cb53a9a8 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   132
    width=5cm,
c498cb53a9a8 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   133
    height=5cm, 
c498cb53a9a8 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   134
    legend entries={Python,Ruby},  
c498cb53a9a8 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   135
    legend pos=north west,
c498cb53a9a8 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   136
    legend cell align=left]
c498cb53a9a8 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   137
\addplot[blue,mark=*, mark options={fill=white}] table {re-python.data};
c498cb53a9a8 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   138
\addplot[brown,mark=triangle*, mark options={fill=white}] table {re-ruby.data};  
c498cb53a9a8 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   139
\end{axis}
c498cb53a9a8 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   140
\end{tikzpicture}
c498cb53a9a8 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   141
&
c498cb53a9a8 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   142
\begin{tikzpicture}
c498cb53a9a8 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   143
  \begin{axis}[
c498cb53a9a8 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   144
    xlabel={$n$},
c498cb53a9a8 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   145
    x label style={at={(1.1,0.05)}},
c498cb53a9a8 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   146
    ylabel={\small time in secs},
c498cb53a9a8 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   147
    enlargelimits=false,
c498cb53a9a8 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   148
    xtick={0,2500,...,11000},
c498cb53a9a8 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   149
    xmax=12000,
c498cb53a9a8 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   150
    ymax=35,
c498cb53a9a8 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   151
    ytick={0,5,...,30},
c498cb53a9a8 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   152
    scaled ticks=false,
c498cb53a9a8 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   153
    axis lines=left,
c498cb53a9a8 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   154
    width=6.5cm,
c498cb53a9a8 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   155
    height=5cm,
c498cb53a9a8 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   156
    legend entries={Derivative matcher},  
c498cb53a9a8 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   157
    legend pos=north east,
c498cb53a9a8 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   158
    legend cell align=left]
c498cb53a9a8 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   159
\addplot[black,mark=square*,mark options={fill=white}] table {re3.data};
c498cb53a9a8 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   160
\end{axis}
c498cb53a9a8 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   161
\end{tikzpicture}
c498cb53a9a8 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   162
\end{tabular}
c498cb53a9a8 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   163
\end{center}
c498cb53a9a8 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   164
c498cb53a9a8 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   165
c498cb53a9a8 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   166
c498cb53a9a8 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   167
\end{document}
c498cb53a9a8 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   168
c498cb53a9a8 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   169
c498cb53a9a8 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   170
c498cb53a9a8 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   171
c498cb53a9a8 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   172
%%% Local Variables: 
c498cb53a9a8 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   173
%%% mode: latex
c498cb53a9a8 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   174
%%% TeX-master: t
c498cb53a9a8 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   175
%%% End: