LMCS-Paper/document/llncs.cls
author Christian Urban <christian dot urban at kcl dot ac dot uk>
Mon, 07 Jul 2014 10:21:40 +0100
changeset 3237 8ee8f72778ce
parent 2985 05ccb61aa628
permissions -rw-r--r--
changed add.assoc
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
2985
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
     1
% LLNCS DOCUMENT CLASS -- version 2.17 (12-Jul-2010)
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
     2
% Springer Verlag LaTeX2e support for Lecture Notes in Computer Science
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
     3
%
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
     4
%%
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
     5
%% \CharacterTable
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
     6
%%  {Upper-case    \A\B\C\D\E\F\G\H\I\J\K\L\M\N\O\P\Q\R\S\T\U\V\W\X\Y\Z
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
     7
%%   Lower-case    \a\b\c\d\e\f\g\h\i\j\k\l\m\n\o\p\q\r\s\t\u\v\w\x\y\z
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
     8
%%   Digits        \0\1\2\3\4\5\6\7\8\9
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
     9
%%   Exclamation   \!     Double quote  \"     Hash (number) \#
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    10
%%   Dollar        \$     Percent       \%     Ampersand     \&
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    11
%%   Acute accent  \'     Left paren    \(     Right paren   \)
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    12
%%   Asterisk      \*     Plus          \+     Comma         \,
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    13
%%   Minus         \-     Point         \.     Solidus       \/
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    14
%%   Colon         \:     Semicolon     \;     Less than     \<
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    15
%%   Equals        \=     Greater than  \>     Question mark \?
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    16
%%   Commercial at \@     Left bracket  \[     Backslash     \\
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    17
%%   Right bracket \]     Circumflex    \^     Underscore    \_
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    18
%%   Grave accent  \`     Left brace    \{     Vertical bar  \|
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    19
%%   Right brace   \}     Tilde         \~}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    20
%%
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    21
\NeedsTeXFormat{LaTeX2e}[1995/12/01]
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    22
\ProvidesClass{llncs}[2010/07/12 v2.17
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    23
^^J LaTeX document class for Lecture Notes in Computer Science]
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    24
% Options
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    25
\let\if@envcntreset\iffalse
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    26
\DeclareOption{envcountreset}{\let\if@envcntreset\iftrue}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    27
\DeclareOption{citeauthoryear}{\let\citeauthoryear=Y}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    28
\DeclareOption{oribibl}{\let\oribibl=Y}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    29
\let\if@custvec\iftrue
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    30
\DeclareOption{orivec}{\let\if@custvec\iffalse}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    31
\let\if@envcntsame\iffalse
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    32
\DeclareOption{envcountsame}{\let\if@envcntsame\iftrue}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    33
\let\if@envcntsect\iffalse
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    34
\DeclareOption{envcountsect}{\let\if@envcntsect\iftrue}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    35
\let\if@runhead\iffalse
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    36
\DeclareOption{runningheads}{\let\if@runhead\iftrue}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    37
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    38
\let\if@openright\iftrue
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    39
\let\if@openbib\iffalse
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    40
\DeclareOption{openbib}{\let\if@openbib\iftrue}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    41
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    42
% languages
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    43
\let\switcht@@therlang\relax
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    44
\def\ds@deutsch{\def\switcht@@therlang{\switcht@deutsch}}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    45
\def\ds@francais{\def\switcht@@therlang{\switcht@francais}}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    46
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    47
\DeclareOption*{\PassOptionsToClass{\CurrentOption}{article}}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    48
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    49
\ProcessOptions
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    50
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    51
\LoadClass[twoside]{article}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    52
\RequirePackage{multicol} % needed for the list of participants, index
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    53
\RequirePackage{aliascnt}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    54
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    55
\setlength{\textwidth}{12.2cm}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    56
\setlength{\textheight}{19.3cm}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    57
\renewcommand\@pnumwidth{2em}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    58
\renewcommand\@tocrmarg{3.5em}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    59
%
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    60
\def\@dottedtocline#1#2#3#4#5{%
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    61
  \ifnum #1>\c@tocdepth \else
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    62
    \vskip \z@ \@plus.2\p@
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    63
    {\leftskip #2\relax \rightskip \@tocrmarg \advance\rightskip by 0pt plus 2cm
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    64
               \parfillskip -\rightskip \pretolerance=10000
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    65
     \parindent #2\relax\@afterindenttrue
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    66
     \interlinepenalty\@M
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    67
     \leavevmode
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    68
     \@tempdima #3\relax
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    69
     \advance\leftskip \@tempdima \null\nobreak\hskip -\leftskip
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    70
     {#4}\nobreak
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    71
     \leaders\hbox{$\m@th
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    72
        \mkern \@dotsep mu\hbox{.}\mkern \@dotsep
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    73
        mu$}\hfill
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    74
     \nobreak
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    75
     \hb@xt@\@pnumwidth{\hfil\normalfont \normalcolor #5}%
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    76
     \par}%
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    77
  \fi}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    78
%
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    79
\def\switcht@albion{%
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    80
\def\abstractname{Abstract.}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    81
\def\ackname{Acknowledgement.}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    82
\def\andname{and}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    83
\def\lastandname{\unskip, and}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    84
\def\appendixname{Appendix}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    85
\def\chaptername{Chapter}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    86
\def\claimname{Claim}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    87
\def\conjecturename{Conjecture}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    88
\def\contentsname{Table of Contents}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    89
\def\corollaryname{Corollary}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    90
\def\definitionname{Definition}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    91
\def\examplename{Example}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    92
\def\exercisename{Exercise}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    93
\def\figurename{Fig.}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    94
\def\keywordname{{\bf Keywords:}}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    95
\def\indexname{Index}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    96
\def\lemmaname{Lemma}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    97
\def\contriblistname{List of Contributors}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    98
\def\listfigurename{List of Figures}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    99
\def\listtablename{List of Tables}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   100
\def\mailname{{\it Correspondence to\/}:}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   101
\def\noteaddname{Note added in proof}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   102
\def\notename{Note}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   103
\def\partname{Part}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   104
\def\problemname{Problem}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   105
\def\proofname{Proof}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   106
\def\propertyname{Property}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   107
\def\propositionname{Proposition}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   108
\def\questionname{Question}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   109
\def\remarkname{Remark}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   110
\def\seename{see}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   111
\def\solutionname{Solution}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   112
\def\subclassname{{\it Subject Classifications\/}:}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   113
\def\tablename{Table}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   114
\def\theoremname{Theorem}}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   115
\switcht@albion
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   116
% Names of theorem like environments are already defined
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   117
% but must be translated if another language is chosen
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   118
%
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   119
% French section
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   120
\def\switcht@francais{%\typeout{On parle francais.}%
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   121
 \def\abstractname{R\'esum\'e.}%
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   122
 \def\ackname{Remerciements.}%
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   123
 \def\andname{et}%
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   124
 \def\lastandname{ et}%
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   125
 \def\appendixname{Appendice}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   126
 \def\chaptername{Chapitre}%
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   127
 \def\claimname{Pr\'etention}%
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   128
 \def\conjecturename{Hypoth\`ese}%
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   129
 \def\contentsname{Table des mati\`eres}%
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   130
 \def\corollaryname{Corollaire}%
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   131
 \def\definitionname{D\'efinition}%
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   132
 \def\examplename{Exemple}%
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   133
 \def\exercisename{Exercice}%
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   134
 \def\figurename{Fig.}%
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   135
 \def\keywordname{{\bf Mots-cl\'e:}}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   136
 \def\indexname{Index}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   137
 \def\lemmaname{Lemme}%
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   138
 \def\contriblistname{Liste des contributeurs}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   139
 \def\listfigurename{Liste des figures}%
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   140
 \def\listtablename{Liste des tables}%
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   141
 \def\mailname{{\it Correspondence to\/}:}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   142
 \def\noteaddname{Note ajout\'ee \`a l'\'epreuve}%
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   143
 \def\notename{Remarque}%
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   144
 \def\partname{Partie}%
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   145
 \def\problemname{Probl\`eme}%
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   146
 \def\proofname{Preuve}%
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   147
 \def\propertyname{Caract\'eristique}%
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   148
%\def\propositionname{Proposition}%
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   149
 \def\questionname{Question}%
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   150
 \def\remarkname{Remarque}%
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   151
 \def\seename{voir}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   152
 \def\solutionname{Solution}%
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   153
 \def\subclassname{{\it Subject Classifications\/}:}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   154
 \def\tablename{Tableau}%
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   155
 \def\theoremname{Th\'eor\`eme}%
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   156
}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   157
%
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   158
% German section
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   159
\def\switcht@deutsch{%\typeout{Man spricht deutsch.}%
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   160
 \def\abstractname{Zusammenfassung.}%
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   161
 \def\ackname{Danksagung.}%
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   162
 \def\andname{und}%
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   163
 \def\lastandname{ und}%
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   164
 \def\appendixname{Anhang}%
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   165
 \def\chaptername{Kapitel}%
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   166
 \def\claimname{Behauptung}%
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   167
 \def\conjecturename{Hypothese}%
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   168
 \def\contentsname{Inhaltsverzeichnis}%
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   169
 \def\corollaryname{Korollar}%
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   170
%\def\definitionname{Definition}%
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   171
 \def\examplename{Beispiel}%
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   172
 \def\exercisename{\"Ubung}%
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   173
 \def\figurename{Abb.}%
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   174
 \def\keywordname{{\bf Schl\"usselw\"orter:}}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   175
 \def\indexname{Index}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   176
%\def\lemmaname{Lemma}%
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   177
 \def\contriblistname{Mitarbeiter}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   178
 \def\listfigurename{Abbildungsverzeichnis}%
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   179
 \def\listtablename{Tabellenverzeichnis}%
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   180
 \def\mailname{{\it Correspondence to\/}:}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   181
 \def\noteaddname{Nachtrag}%
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   182
 \def\notename{Anmerkung}%
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   183
 \def\partname{Teil}%
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   184
%\def\problemname{Problem}%
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   185
 \def\proofname{Beweis}%
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   186
 \def\propertyname{Eigenschaft}%
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   187
%\def\propositionname{Proposition}%
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   188
 \def\questionname{Frage}%
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   189
 \def\remarkname{Anmerkung}%
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   190
 \def\seename{siehe}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   191
 \def\solutionname{L\"osung}%
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   192
 \def\subclassname{{\it Subject Classifications\/}:}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   193
 \def\tablename{Tabelle}%
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   194
%\def\theoremname{Theorem}%
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   195
}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   196
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   197
% Ragged bottom for the actual page
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   198
\def\thisbottomragged{\def\@textbottom{\vskip\z@ plus.0001fil
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   199
\global\let\@textbottom\relax}}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   200
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   201
\renewcommand\small{%
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   202
   \@setfontsize\small\@ixpt{11}%
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   203
   \abovedisplayskip 8.5\p@ \@plus3\p@ \@minus4\p@
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   204
   \abovedisplayshortskip \z@ \@plus2\p@
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   205
   \belowdisplayshortskip 4\p@ \@plus2\p@ \@minus2\p@
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   206
   \def\@listi{\leftmargin\leftmargini
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   207
               \parsep 0\p@ \@plus1\p@ \@minus\p@
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   208
               \topsep 8\p@ \@plus2\p@ \@minus4\p@
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   209
               \itemsep0\p@}%
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   210
   \belowdisplayskip \abovedisplayskip
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   211
}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   212
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   213
\frenchspacing
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   214
\widowpenalty=10000
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   215
\clubpenalty=10000
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   216
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   217
\setlength\oddsidemargin   {63\p@}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   218
\setlength\evensidemargin  {63\p@}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   219
\setlength\marginparwidth  {90\p@}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   220
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   221
\setlength\headsep   {16\p@}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   222
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   223
\setlength\footnotesep{7.7\p@}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   224
\setlength\textfloatsep{8mm\@plus 2\p@ \@minus 4\p@}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   225
\setlength\intextsep   {8mm\@plus 2\p@ \@minus 2\p@}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   226
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   227
\setcounter{secnumdepth}{2}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   228
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   229
\newcounter {chapter}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   230
\renewcommand\thechapter      {\@arabic\c@chapter}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   231
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   232
\newif\if@mainmatter \@mainmattertrue
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   233
\newcommand\frontmatter{\cleardoublepage
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   234
            \@mainmatterfalse\pagenumbering{Roman}}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   235
\newcommand\mainmatter{\cleardoublepage
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   236
       \@mainmattertrue\pagenumbering{arabic}}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   237
\newcommand\backmatter{\if@openright\cleardoublepage\else\clearpage\fi
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   238
      \@mainmatterfalse}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   239
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   240
\renewcommand\part{\cleardoublepage
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   241
                 \thispagestyle{empty}%
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   242
                 \if@twocolumn
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   243
                     \onecolumn
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   244
                     \@tempswatrue
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   245
                   \else
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   246
                     \@tempswafalse
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   247
                 \fi
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   248
                 \null\vfil
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   249
                 \secdef\@part\@spart}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   250
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   251
\def\@part[#1]#2{%
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   252
    \ifnum \c@secnumdepth >-2\relax
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   253
      \refstepcounter{part}%
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   254
      \addcontentsline{toc}{part}{\thepart\hspace{1em}#1}%
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   255
    \else
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   256
      \addcontentsline{toc}{part}{#1}%
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   257
    \fi
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   258
    \markboth{}{}%
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   259
    {\centering
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   260
     \interlinepenalty \@M
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   261
     \normalfont
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   262
     \ifnum \c@secnumdepth >-2\relax
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   263
       \huge\bfseries \partname~\thepart
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   264
       \par
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   265
       \vskip 20\p@
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   266
     \fi
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   267
     \Huge \bfseries #2\par}%
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   268
    \@endpart}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   269
\def\@spart#1{%
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   270
    {\centering
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   271
     \interlinepenalty \@M
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   272
     \normalfont
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   273
     \Huge \bfseries #1\par}%
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   274
    \@endpart}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   275
\def\@endpart{\vfil\newpage
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   276
              \if@twoside
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   277
                \null
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   278
                \thispagestyle{empty}%
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   279
                \newpage
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   280
              \fi
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   281
              \if@tempswa
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   282
                \twocolumn
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   283
              \fi}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   284
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   285
\newcommand\chapter{\clearpage
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   286
                    \thispagestyle{empty}%
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   287
                    \global\@topnum\z@
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   288
                    \@afterindentfalse
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   289
                    \secdef\@chapter\@schapter}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   290
\def\@chapter[#1]#2{\ifnum \c@secnumdepth >\m@ne
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   291
                       \if@mainmatter
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   292
                         \refstepcounter{chapter}%
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   293
                         \typeout{\@chapapp\space\thechapter.}%
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   294
                         \addcontentsline{toc}{chapter}%
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   295
                                  {\protect\numberline{\thechapter}#1}%
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   296
                       \else
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   297
                         \addcontentsline{toc}{chapter}{#1}%
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   298
                       \fi
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   299
                    \else
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   300
                      \addcontentsline{toc}{chapter}{#1}%
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   301
                    \fi
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   302
                    \chaptermark{#1}%
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   303
                    \addtocontents{lof}{\protect\addvspace{10\p@}}%
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   304
                    \addtocontents{lot}{\protect\addvspace{10\p@}}%
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   305
                    \if@twocolumn
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   306
                      \@topnewpage[\@makechapterhead{#2}]%
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   307
                    \else
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   308
                      \@makechapterhead{#2}%
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   309
                      \@afterheading
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   310
                    \fi}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   311
\def\@makechapterhead#1{%
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   312
% \vspace*{50\p@}%
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   313
  {\centering
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   314
    \ifnum \c@secnumdepth >\m@ne
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   315
      \if@mainmatter
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   316
        \large\bfseries \@chapapp{} \thechapter
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   317
        \par\nobreak
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   318
        \vskip 20\p@
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   319
      \fi
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   320
    \fi
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   321
    \interlinepenalty\@M
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   322
    \Large \bfseries #1\par\nobreak
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   323
    \vskip 40\p@
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   324
  }}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   325
\def\@schapter#1{\if@twocolumn
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   326
                   \@topnewpage[\@makeschapterhead{#1}]%
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   327
                 \else
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   328
                   \@makeschapterhead{#1}%
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   329
                   \@afterheading
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   330
                 \fi}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   331
\def\@makeschapterhead#1{%
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   332
% \vspace*{50\p@}%
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   333
  {\centering
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   334
    \normalfont
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   335
    \interlinepenalty\@M
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   336
    \Large \bfseries  #1\par\nobreak
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   337
    \vskip 40\p@
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   338
  }}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   339
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   340
\renewcommand\section{\@startsection{section}{1}{\z@}%
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   341
                       {-18\p@ \@plus -4\p@ \@minus -4\p@}%
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   342
                       {12\p@ \@plus 4\p@ \@minus 4\p@}%
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   343
                       {\normalfont\large\bfseries\boldmath
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   344
                        \rightskip=\z@ \@plus 8em\pretolerance=10000 }}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   345
\renewcommand\subsection{\@startsection{subsection}{2}{\z@}%
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   346
                       {-18\p@ \@plus -4\p@ \@minus -4\p@}%
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   347
                       {8\p@ \@plus 4\p@ \@minus 4\p@}%
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   348
                       {\normalfont\normalsize\bfseries\boldmath
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   349
                        \rightskip=\z@ \@plus 8em\pretolerance=10000 }}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   350
\renewcommand\subsubsection{\@startsection{subsubsection}{3}{\z@}%
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   351
                       {-18\p@ \@plus -4\p@ \@minus -4\p@}%
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   352
                       {-0.5em \@plus -0.22em \@minus -0.1em}%
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   353
                       {\normalfont\normalsize\bfseries\boldmath}}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   354
\renewcommand\paragraph{\@startsection{paragraph}{4}{\z@}%
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   355
                       {-12\p@ \@plus -4\p@ \@minus -4\p@}%
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   356
                       {-0.5em \@plus -0.22em \@minus -0.1em}%
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   357
                       {\normalfont\normalsize\itshape}}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   358
\renewcommand\subparagraph[1]{\typeout{LLNCS warning: You should not use
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   359
                  \string\subparagraph\space with this class}\vskip0.5cm
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   360
You should not use \verb|\subparagraph| with this class.\vskip0.5cm}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   361
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   362
\DeclareMathSymbol{\Gamma}{\mathalpha}{letters}{"00}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   363
\DeclareMathSymbol{\Delta}{\mathalpha}{letters}{"01}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   364
\DeclareMathSymbol{\Theta}{\mathalpha}{letters}{"02}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   365
\DeclareMathSymbol{\Lambda}{\mathalpha}{letters}{"03}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   366
\DeclareMathSymbol{\Xi}{\mathalpha}{letters}{"04}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   367
\DeclareMathSymbol{\Pi}{\mathalpha}{letters}{"05}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   368
\DeclareMathSymbol{\Sigma}{\mathalpha}{letters}{"06}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   369
\DeclareMathSymbol{\Upsilon}{\mathalpha}{letters}{"07}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   370
\DeclareMathSymbol{\Phi}{\mathalpha}{letters}{"08}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   371
\DeclareMathSymbol{\Psi}{\mathalpha}{letters}{"09}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   372
\DeclareMathSymbol{\Omega}{\mathalpha}{letters}{"0A}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   373
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   374
\let\footnotesize\small
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   375
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   376
\if@custvec
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   377
\def\vec#1{\mathchoice{\mbox{\boldmath$\displaystyle#1$}}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   378
{\mbox{\boldmath$\textstyle#1$}}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   379
{\mbox{\boldmath$\scriptstyle#1$}}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   380
{\mbox{\boldmath$\scriptscriptstyle#1$}}}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   381
\fi
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   382
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   383
\def\squareforqed{\hbox{\rlap{$\sqcap$}$\sqcup$}}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   384
\def\qed{\ifmmode\squareforqed\else{\unskip\nobreak\hfil
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   385
\penalty50\hskip1em\null\nobreak\hfil\squareforqed
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   386
\parfillskip=0pt\finalhyphendemerits=0\endgraf}\fi}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   387
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   388
\def\getsto{\mathrel{\mathchoice {\vcenter{\offinterlineskip
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   389
\halign{\hfil
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   390
$\displaystyle##$\hfil\cr\gets\cr\to\cr}}}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   391
{\vcenter{\offinterlineskip\halign{\hfil$\textstyle##$\hfil\cr\gets
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   392
\cr\to\cr}}}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   393
{\vcenter{\offinterlineskip\halign{\hfil$\scriptstyle##$\hfil\cr\gets
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   394
\cr\to\cr}}}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   395
{\vcenter{\offinterlineskip\halign{\hfil$\scriptscriptstyle##$\hfil\cr
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   396
\gets\cr\to\cr}}}}}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   397
\def\lid{\mathrel{\mathchoice {\vcenter{\offinterlineskip\halign{\hfil
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   398
$\displaystyle##$\hfil\cr<\cr\noalign{\vskip1.2pt}=\cr}}}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   399
{\vcenter{\offinterlineskip\halign{\hfil$\textstyle##$\hfil\cr<\cr
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   400
\noalign{\vskip1.2pt}=\cr}}}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   401
{\vcenter{\offinterlineskip\halign{\hfil$\scriptstyle##$\hfil\cr<\cr
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   402
\noalign{\vskip1pt}=\cr}}}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   403
{\vcenter{\offinterlineskip\halign{\hfil$\scriptscriptstyle##$\hfil\cr
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   404
<\cr
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   405
\noalign{\vskip0.9pt}=\cr}}}}}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   406
\def\gid{\mathrel{\mathchoice {\vcenter{\offinterlineskip\halign{\hfil
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   407
$\displaystyle##$\hfil\cr>\cr\noalign{\vskip1.2pt}=\cr}}}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   408
{\vcenter{\offinterlineskip\halign{\hfil$\textstyle##$\hfil\cr>\cr
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   409
\noalign{\vskip1.2pt}=\cr}}}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   410
{\vcenter{\offinterlineskip\halign{\hfil$\scriptstyle##$\hfil\cr>\cr
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   411
\noalign{\vskip1pt}=\cr}}}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   412
{\vcenter{\offinterlineskip\halign{\hfil$\scriptscriptstyle##$\hfil\cr
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   413
>\cr
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   414
\noalign{\vskip0.9pt}=\cr}}}}}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   415
\def\grole{\mathrel{\mathchoice {\vcenter{\offinterlineskip
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   416
\halign{\hfil
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   417
$\displaystyle##$\hfil\cr>\cr\noalign{\vskip-1pt}<\cr}}}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   418
{\vcenter{\offinterlineskip\halign{\hfil$\textstyle##$\hfil\cr
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   419
>\cr\noalign{\vskip-1pt}<\cr}}}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   420
{\vcenter{\offinterlineskip\halign{\hfil$\scriptstyle##$\hfil\cr
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   421
>\cr\noalign{\vskip-0.8pt}<\cr}}}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   422
{\vcenter{\offinterlineskip\halign{\hfil$\scriptscriptstyle##$\hfil\cr
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   423
>\cr\noalign{\vskip-0.3pt}<\cr}}}}}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   424
\def\bbbr{{\rm I\!R}} %reelle Zahlen
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   425
\def\bbbm{{\rm I\!M}}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   426
\def\bbbn{{\rm I\!N}} %natuerliche Zahlen
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   427
\def\bbbf{{\rm I\!F}}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   428
\def\bbbh{{\rm I\!H}}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   429
\def\bbbk{{\rm I\!K}}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   430
\def\bbbp{{\rm I\!P}}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   431
\def\bbbone{{\mathchoice {\rm 1\mskip-4mu l} {\rm 1\mskip-4mu l}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   432
{\rm 1\mskip-4.5mu l} {\rm 1\mskip-5mu l}}}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   433
\def\bbbc{{\mathchoice {\setbox0=\hbox{$\displaystyle\rm C$}\hbox{\hbox
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   434
to0pt{\kern0.4\wd0\vrule height0.9\ht0\hss}\box0}}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   435
{\setbox0=\hbox{$\textstyle\rm C$}\hbox{\hbox
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   436
to0pt{\kern0.4\wd0\vrule height0.9\ht0\hss}\box0}}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   437
{\setbox0=\hbox{$\scriptstyle\rm C$}\hbox{\hbox
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   438
to0pt{\kern0.4\wd0\vrule height0.9\ht0\hss}\box0}}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   439
{\setbox0=\hbox{$\scriptscriptstyle\rm C$}\hbox{\hbox
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   440
to0pt{\kern0.4\wd0\vrule height0.9\ht0\hss}\box0}}}}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   441
\def\bbbq{{\mathchoice {\setbox0=\hbox{$\displaystyle\rm
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   442
Q$}\hbox{\raise
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   443
0.15\ht0\hbox to0pt{\kern0.4\wd0\vrule height0.8\ht0\hss}\box0}}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   444
{\setbox0=\hbox{$\textstyle\rm Q$}\hbox{\raise
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   445
0.15\ht0\hbox to0pt{\kern0.4\wd0\vrule height0.8\ht0\hss}\box0}}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   446
{\setbox0=\hbox{$\scriptstyle\rm Q$}\hbox{\raise
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   447
0.15\ht0\hbox to0pt{\kern0.4\wd0\vrule height0.7\ht0\hss}\box0}}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   448
{\setbox0=\hbox{$\scriptscriptstyle\rm Q$}\hbox{\raise
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   449
0.15\ht0\hbox to0pt{\kern0.4\wd0\vrule height0.7\ht0\hss}\box0}}}}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   450
\def\bbbt{{\mathchoice {\setbox0=\hbox{$\displaystyle\rm
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   451
T$}\hbox{\hbox to0pt{\kern0.3\wd0\vrule height0.9\ht0\hss}\box0}}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   452
{\setbox0=\hbox{$\textstyle\rm T$}\hbox{\hbox
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   453
to0pt{\kern0.3\wd0\vrule height0.9\ht0\hss}\box0}}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   454
{\setbox0=\hbox{$\scriptstyle\rm T$}\hbox{\hbox
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   455
to0pt{\kern0.3\wd0\vrule height0.9\ht0\hss}\box0}}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   456
{\setbox0=\hbox{$\scriptscriptstyle\rm T$}\hbox{\hbox
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   457
to0pt{\kern0.3\wd0\vrule height0.9\ht0\hss}\box0}}}}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   458
\def\bbbs{{\mathchoice
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   459
{\setbox0=\hbox{$\displaystyle     \rm S$}\hbox{\raise0.5\ht0\hbox
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   460
to0pt{\kern0.35\wd0\vrule height0.45\ht0\hss}\hbox
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   461
to0pt{\kern0.55\wd0\vrule height0.5\ht0\hss}\box0}}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   462
{\setbox0=\hbox{$\textstyle        \rm S$}\hbox{\raise0.5\ht0\hbox
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   463
to0pt{\kern0.35\wd0\vrule height0.45\ht0\hss}\hbox
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   464
to0pt{\kern0.55\wd0\vrule height0.5\ht0\hss}\box0}}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   465
{\setbox0=\hbox{$\scriptstyle      \rm S$}\hbox{\raise0.5\ht0\hbox
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   466
to0pt{\kern0.35\wd0\vrule height0.45\ht0\hss}\raise0.05\ht0\hbox
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   467
to0pt{\kern0.5\wd0\vrule height0.45\ht0\hss}\box0}}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   468
{\setbox0=\hbox{$\scriptscriptstyle\rm S$}\hbox{\raise0.5\ht0\hbox
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   469
to0pt{\kern0.4\wd0\vrule height0.45\ht0\hss}\raise0.05\ht0\hbox
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   470
to0pt{\kern0.55\wd0\vrule height0.45\ht0\hss}\box0}}}}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   471
\def\bbbz{{\mathchoice {\hbox{$\mathsf\textstyle Z\kern-0.4em Z$}}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   472
{\hbox{$\mathsf\textstyle Z\kern-0.4em Z$}}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   473
{\hbox{$\mathsf\scriptstyle Z\kern-0.3em Z$}}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   474
{\hbox{$\mathsf\scriptscriptstyle Z\kern-0.2em Z$}}}}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   475
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   476
\let\ts\,
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   477
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   478
\setlength\leftmargini  {17\p@}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   479
\setlength\leftmargin    {\leftmargini}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   480
\setlength\leftmarginii  {\leftmargini}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   481
\setlength\leftmarginiii {\leftmargini}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   482
\setlength\leftmarginiv  {\leftmargini}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   483
\setlength  \labelsep  {.5em}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   484
\setlength  \labelwidth{\leftmargini}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   485
\addtolength\labelwidth{-\labelsep}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   486
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   487
\def\@listI{\leftmargin\leftmargini
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   488
            \parsep 0\p@ \@plus1\p@ \@minus\p@
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   489
            \topsep 8\p@ \@plus2\p@ \@minus4\p@
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   490
            \itemsep0\p@}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   491
\let\@listi\@listI
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   492
\@listi
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   493
\def\@listii {\leftmargin\leftmarginii
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   494
              \labelwidth\leftmarginii
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   495
              \advance\labelwidth-\labelsep
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   496
              \topsep    0\p@ \@plus2\p@ \@minus\p@}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   497
\def\@listiii{\leftmargin\leftmarginiii
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   498
              \labelwidth\leftmarginiii
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   499
              \advance\labelwidth-\labelsep
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   500
              \topsep    0\p@ \@plus\p@\@minus\p@
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   501
              \parsep    \z@
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   502
              \partopsep \p@ \@plus\z@ \@minus\p@}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   503
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   504
\renewcommand\labelitemi{\normalfont\bfseries --}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   505
\renewcommand\labelitemii{$\m@th\bullet$}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   506
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   507
\setlength\arraycolsep{1.4\p@}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   508
\setlength\tabcolsep{1.4\p@}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   509
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   510
\def\tableofcontents{\chapter*{\contentsname\@mkboth{{\contentsname}}%
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   511
                                                    {{\contentsname}}}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   512
 \def\authcount##1{\setcounter{auco}{##1}\setcounter{@auth}{1}}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   513
 \def\lastand{\ifnum\value{auco}=2\relax
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   514
                 \unskip{} \andname\
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   515
              \else
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   516
                 \unskip \lastandname\
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   517
              \fi}%
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   518
 \def\and{\stepcounter{@auth}\relax
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   519
          \ifnum\value{@auth}=\value{auco}%
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   520
             \lastand
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   521
          \else
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   522
             \unskip,
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   523
          \fi}%
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   524
 \@starttoc{toc}\if@restonecol\twocolumn\fi}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   525
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   526
\def\l@part#1#2{\addpenalty{\@secpenalty}%
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   527
   \addvspace{2em plus\p@}%  % space above part line
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   528
   \begingroup
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   529
     \parindent \z@
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   530
     \rightskip \z@ plus 5em
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   531
     \hrule\vskip5pt
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   532
     \large               % same size as for a contribution heading
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   533
     \bfseries\boldmath   % set line in boldface
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   534
     \leavevmode          % TeX command to enter horizontal mode.
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   535
     #1\par
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   536
     \vskip5pt
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   537
     \hrule
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   538
     \vskip1pt
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   539
     \nobreak             % Never break after part entry
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   540
   \endgroup}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   541
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   542
\def\@dotsep{2}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   543
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   544
\let\phantomsection=\relax
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   545
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   546
\def\hyperhrefextend{\ifx\hyper@anchor\@undefined\else
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   547
{}\fi}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   548
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   549
\def\addnumcontentsmark#1#2#3{%
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   550
\addtocontents{#1}{\protect\contentsline{#2}{\protect\numberline
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   551
                     {\thechapter}#3}{\thepage}\hyperhrefextend}}%
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   552
\def\addcontentsmark#1#2#3{%
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   553
\addtocontents{#1}{\protect\contentsline{#2}{#3}{\thepage}\hyperhrefextend}}%
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   554
\def\addcontentsmarkwop#1#2#3{%
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   555
\addtocontents{#1}{\protect\contentsline{#2}{#3}{0}\hyperhrefextend}}%
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   556
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   557
\def\@adcmk[#1]{\ifcase #1 \or
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   558
\def\@gtempa{\addnumcontentsmark}%
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   559
  \or    \def\@gtempa{\addcontentsmark}%
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   560
  \or    \def\@gtempa{\addcontentsmarkwop}%
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   561
  \fi\@gtempa{toc}{chapter}%
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   562
}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   563
\def\addtocmark{%
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   564
\phantomsection
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   565
\@ifnextchar[{\@adcmk}{\@adcmk[3]}%
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   566
}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   567
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   568
\def\l@chapter#1#2{\addpenalty{-\@highpenalty}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   569
 \vskip 1.0em plus 1pt \@tempdima 1.5em \begingroup
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   570
 \parindent \z@ \rightskip \@tocrmarg
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   571
 \advance\rightskip by 0pt plus 2cm
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   572
 \parfillskip -\rightskip \pretolerance=10000
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   573
 \leavevmode \advance\leftskip\@tempdima \hskip -\leftskip
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   574
 {\large\bfseries\boldmath#1}\ifx0#2\hfil\null
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   575
 \else
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   576
      \nobreak
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   577
      \leaders\hbox{$\m@th \mkern \@dotsep mu.\mkern
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   578
      \@dotsep mu$}\hfill
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   579
      \nobreak\hbox to\@pnumwidth{\hss #2}%
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   580
 \fi\par
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   581
 \penalty\@highpenalty \endgroup}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   582
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   583
\def\l@title#1#2{\addpenalty{-\@highpenalty}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   584
 \addvspace{8pt plus 1pt}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   585
 \@tempdima \z@
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   586
 \begingroup
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   587
 \parindent \z@ \rightskip \@tocrmarg
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   588
 \advance\rightskip by 0pt plus 2cm
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   589
 \parfillskip -\rightskip \pretolerance=10000
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   590
 \leavevmode \advance\leftskip\@tempdima \hskip -\leftskip
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   591
 #1\nobreak
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   592
 \leaders\hbox{$\m@th \mkern \@dotsep mu.\mkern
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   593
 \@dotsep mu$}\hfill
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   594
 \nobreak\hbox to\@pnumwidth{\hss #2}\par
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   595
 \penalty\@highpenalty \endgroup}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   596
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   597
\def\l@author#1#2{\addpenalty{\@highpenalty}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   598
 \@tempdima=15\p@ %\z@
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   599
 \begingroup
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   600
 \parindent \z@ \rightskip \@tocrmarg
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   601
 \advance\rightskip by 0pt plus 2cm
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   602
 \pretolerance=10000
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   603
 \leavevmode \advance\leftskip\@tempdima %\hskip -\leftskip
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   604
 \textit{#1}\par
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   605
 \penalty\@highpenalty \endgroup}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   606
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   607
\setcounter{tocdepth}{0}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   608
\newdimen\tocchpnum
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   609
\newdimen\tocsecnum
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   610
\newdimen\tocsectotal
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   611
\newdimen\tocsubsecnum
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   612
\newdimen\tocsubsectotal
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   613
\newdimen\tocsubsubsecnum
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   614
\newdimen\tocsubsubsectotal
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   615
\newdimen\tocparanum
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   616
\newdimen\tocparatotal
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   617
\newdimen\tocsubparanum
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   618
\tocchpnum=\z@            % no chapter numbers
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   619
\tocsecnum=15\p@          % section 88. plus 2.222pt
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   620
\tocsubsecnum=23\p@       % subsection 88.8 plus 2.222pt
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   621
\tocsubsubsecnum=27\p@    % subsubsection 88.8.8 plus 1.444pt
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   622
\tocparanum=35\p@         % paragraph 88.8.8.8 plus 1.666pt
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   623
\tocsubparanum=43\p@      % subparagraph 88.8.8.8.8 plus 1.888pt
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   624
\def\calctocindent{%
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   625
\tocsectotal=\tocchpnum
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   626
\advance\tocsectotal by\tocsecnum
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   627
\tocsubsectotal=\tocsectotal
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   628
\advance\tocsubsectotal by\tocsubsecnum
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   629
\tocsubsubsectotal=\tocsubsectotal
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   630
\advance\tocsubsubsectotal by\tocsubsubsecnum
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   631
\tocparatotal=\tocsubsubsectotal
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   632
\advance\tocparatotal by\tocparanum}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   633
\calctocindent
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   634
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   635
\def\l@section{\@dottedtocline{1}{\tocchpnum}{\tocsecnum}}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   636
\def\l@subsection{\@dottedtocline{2}{\tocsectotal}{\tocsubsecnum}}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   637
\def\l@subsubsection{\@dottedtocline{3}{\tocsubsectotal}{\tocsubsubsecnum}}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   638
\def\l@paragraph{\@dottedtocline{4}{\tocsubsubsectotal}{\tocparanum}}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   639
\def\l@subparagraph{\@dottedtocline{5}{\tocparatotal}{\tocsubparanum}}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   640
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   641
\def\listoffigures{\@restonecolfalse\if@twocolumn\@restonecoltrue\onecolumn
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   642
 \fi\section*{\listfigurename\@mkboth{{\listfigurename}}{{\listfigurename}}}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   643
 \@starttoc{lof}\if@restonecol\twocolumn\fi}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   644
\def\l@figure{\@dottedtocline{1}{0em}{1.5em}}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   645
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   646
\def\listoftables{\@restonecolfalse\if@twocolumn\@restonecoltrue\onecolumn
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   647
 \fi\section*{\listtablename\@mkboth{{\listtablename}}{{\listtablename}}}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   648
 \@starttoc{lot}\if@restonecol\twocolumn\fi}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   649
\let\l@table\l@figure
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   650
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   651
\renewcommand\listoffigures{%
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   652
    \section*{\listfigurename
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   653
      \@mkboth{\listfigurename}{\listfigurename}}%
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   654
    \@starttoc{lof}%
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   655
    }
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   656
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   657
\renewcommand\listoftables{%
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   658
    \section*{\listtablename
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   659
      \@mkboth{\listtablename}{\listtablename}}%
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   660
    \@starttoc{lot}%
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   661
    }
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   662
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   663
\ifx\oribibl\undefined
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   664
\ifx\citeauthoryear\undefined
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   665
\renewenvironment{thebibliography}[1]
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   666
     {\section*{\refname}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   667
      \def\@biblabel##1{##1.}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   668
      \small
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   669
      \list{\@biblabel{\@arabic\c@enumiv}}%
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   670
           {\settowidth\labelwidth{\@biblabel{#1}}%
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   671
            \leftmargin\labelwidth
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   672
            \advance\leftmargin\labelsep
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   673
            \if@openbib
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   674
              \advance\leftmargin\bibindent
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   675
              \itemindent -\bibindent
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   676
              \listparindent \itemindent
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   677
              \parsep \z@
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   678
            \fi
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   679
            \usecounter{enumiv}%
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   680
            \let\p@enumiv\@empty
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   681
            \renewcommand\theenumiv{\@arabic\c@enumiv}}%
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   682
      \if@openbib
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   683
        \renewcommand\newblock{\par}%
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   684
      \else
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   685
        \renewcommand\newblock{\hskip .11em \@plus.33em \@minus.07em}%
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   686
      \fi
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   687
      \sloppy\clubpenalty4000\widowpenalty4000%
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   688
      \sfcode`\.=\@m}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   689
     {\def\@noitemerr
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   690
       {\@latex@warning{Empty `thebibliography' environment}}%
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   691
      \endlist}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   692
\def\@lbibitem[#1]#2{\item[{[#1]}\hfill]\if@filesw
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   693
     {\let\protect\noexpand\immediate
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   694
     \write\@auxout{\string\bibcite{#2}{#1}}}\fi\ignorespaces}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   695
\newcount\@tempcntc
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   696
\def\@citex[#1]#2{\if@filesw\immediate\write\@auxout{\string\citation{#2}}\fi
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   697
  \@tempcnta\z@\@tempcntb\m@ne\def\@citea{}\@cite{\@for\@citeb:=#2\do
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   698
    {\@ifundefined
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   699
       {b@\@citeb}{\@citeo\@tempcntb\m@ne\@citea\def\@citea{,}{\bfseries
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   700
        ?}\@warning
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   701
       {Citation `\@citeb' on page \thepage \space undefined}}%
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   702
    {\setbox\z@\hbox{\global\@tempcntc0\csname b@\@citeb\endcsname\relax}%
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   703
     \ifnum\@tempcntc=\z@ \@citeo\@tempcntb\m@ne
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   704
       \@citea\def\@citea{,}\hbox{\csname b@\@citeb\endcsname}%
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   705
     \else
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   706
      \advance\@tempcntb\@ne
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   707
      \ifnum\@tempcntb=\@tempcntc
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   708
      \else\advance\@tempcntb\m@ne\@citeo
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   709
      \@tempcnta\@tempcntc\@tempcntb\@tempcntc\fi\fi}}\@citeo}{#1}}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   710
\def\@citeo{\ifnum\@tempcnta>\@tempcntb\else
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   711
               \@citea\def\@citea{,\,\hskip\z@skip}%
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   712
               \ifnum\@tempcnta=\@tempcntb\the\@tempcnta\else
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   713
               {\advance\@tempcnta\@ne\ifnum\@tempcnta=\@tempcntb \else
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   714
                \def\@citea{--}\fi
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   715
      \advance\@tempcnta\m@ne\the\@tempcnta\@citea\the\@tempcntb}\fi\fi}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   716
\else
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   717
\renewenvironment{thebibliography}[1]
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   718
     {\section*{\refname}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   719
      \small
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   720
      \list{}%
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   721
           {\settowidth\labelwidth{}%
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   722
            \leftmargin\parindent
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   723
            \itemindent=-\parindent
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   724
            \labelsep=\z@
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   725
            \if@openbib
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   726
              \advance\leftmargin\bibindent
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   727
              \itemindent -\bibindent
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   728
              \listparindent \itemindent
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   729
              \parsep \z@
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   730
            \fi
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   731
            \usecounter{enumiv}%
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   732
            \let\p@enumiv\@empty
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   733
            \renewcommand\theenumiv{}}%
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   734
      \if@openbib
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   735
        \renewcommand\newblock{\par}%
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   736
      \else
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   737
        \renewcommand\newblock{\hskip .11em \@plus.33em \@minus.07em}%
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   738
      \fi
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   739
      \sloppy\clubpenalty4000\widowpenalty4000%
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   740
      \sfcode`\.=\@m}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   741
     {\def\@noitemerr
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   742
       {\@latex@warning{Empty `thebibliography' environment}}%
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   743
      \endlist}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   744
      \def\@cite#1{#1}%
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   745
      \def\@lbibitem[#1]#2{\item[]\if@filesw
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   746
        {\def\protect##1{\string ##1\space}\immediate
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   747
      \write\@auxout{\string\bibcite{#2}{#1}}}\fi\ignorespaces}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   748
   \fi
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   749
\else
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   750
\@cons\@openbib@code{\noexpand\small}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   751
\fi
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   752
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   753
\def\idxquad{\hskip 10\p@}% space that divides entry from number
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   754
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   755
\def\@idxitem{\par\hangindent 10\p@}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   756
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   757
\def\subitem{\par\setbox0=\hbox{--\enspace}% second order
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   758
                \noindent\hangindent\wd0\box0}% index entry
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   759
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   760
\def\subsubitem{\par\setbox0=\hbox{--\,--\enspace}% third
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   761
                \noindent\hangindent\wd0\box0}% order index entry
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   762
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   763
\def\indexspace{\par \vskip 10\p@ plus5\p@ minus3\p@\relax}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   764
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   765
\renewenvironment{theindex}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   766
               {\@mkboth{\indexname}{\indexname}%
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   767
                \thispagestyle{empty}\parindent\z@
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   768
                \parskip\z@ \@plus .3\p@\relax
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   769
                \let\item\par
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   770
                \def\,{\relax\ifmmode\mskip\thinmuskip
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   771
                             \else\hskip0.2em\ignorespaces\fi}%
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   772
                \normalfont\small
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   773
                \begin{multicols}{2}[\@makeschapterhead{\indexname}]%
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   774
                }
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   775
                {\end{multicols}}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   776
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   777
\renewcommand\footnoterule{%
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   778
  \kern-3\p@
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   779
  \hrule\@width 2truecm
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   780
  \kern2.6\p@}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   781
  \newdimen\fnindent
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   782
  \fnindent1em
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   783
\long\def\@makefntext#1{%
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   784
    \parindent \fnindent%
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   785
    \leftskip \fnindent%
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   786
    \noindent
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   787
    \llap{\hb@xt@1em{\hss\@makefnmark\ }}\ignorespaces#1}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   788
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   789
\long\def\@makecaption#1#2{%
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   790
  \small
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   791
  \vskip\abovecaptionskip
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   792
  \sbox\@tempboxa{{\bfseries #1.} #2}%
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   793
  \ifdim \wd\@tempboxa >\hsize
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   794
    {\bfseries #1.} #2\par
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   795
  \else
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   796
    \global \@minipagefalse
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   797
    \hb@xt@\hsize{\hfil\box\@tempboxa\hfil}%
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   798
  \fi
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   799
  \vskip\belowcaptionskip}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   800
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   801
\def\fps@figure{htbp}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   802
\def\fnum@figure{\figurename\thinspace\thefigure}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   803
\def \@floatboxreset {%
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   804
        \reset@font
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   805
        \small
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   806
        \@setnobreak
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   807
        \@setminipage
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   808
}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   809
\def\fps@table{htbp}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   810
\def\fnum@table{\tablename~\thetable}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   811
\renewenvironment{table}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   812
               {\setlength\abovecaptionskip{0\p@}%
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   813
                \setlength\belowcaptionskip{10\p@}%
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   814
                \@float{table}}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   815
               {\end@float}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   816
\renewenvironment{table*}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   817
               {\setlength\abovecaptionskip{0\p@}%
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   818
                \setlength\belowcaptionskip{10\p@}%
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   819
                \@dblfloat{table}}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   820
               {\end@dblfloat}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   821
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   822
\long\def\@caption#1[#2]#3{\par\addcontentsline{\csname
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   823
  ext@#1\endcsname}{#1}{\protect\numberline{\csname
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   824
  the#1\endcsname}{\ignorespaces #2}}\begingroup
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   825
    \@parboxrestore
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   826
    \@makecaption{\csname fnum@#1\endcsname}{\ignorespaces #3}\par
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   827
  \endgroup}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   828
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   829
% LaTeX does not provide a command to enter the authors institute
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   830
% addresses. The \institute command is defined here.
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   831
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   832
\newcounter{@inst}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   833
\newcounter{@auth}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   834
\newcounter{auco}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   835
\newdimen\instindent
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   836
\newbox\authrun
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   837
\newtoks\authorrunning
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   838
\newtoks\tocauthor
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   839
\newbox\titrun
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   840
\newtoks\titlerunning
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   841
\newtoks\toctitle
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   842
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   843
\def\clearheadinfo{\gdef\@author{No Author Given}%
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   844
                   \gdef\@title{No Title Given}%
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   845
                   \gdef\@subtitle{}%
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   846
                   \gdef\@institute{No Institute Given}%
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   847
                   \gdef\@thanks{}%
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   848
                   \global\titlerunning={}\global\authorrunning={}%
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   849
                   \global\toctitle={}\global\tocauthor={}}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   850
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   851
\def\institute#1{\gdef\@institute{#1}}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   852
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   853
\def\institutename{\par
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   854
 \begingroup
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   855
 \parskip=\z@
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   856
 \parindent=\z@
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   857
 \setcounter{@inst}{1}%
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   858
 \def\and{\par\stepcounter{@inst}%
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   859
 \noindent$^{\the@inst}$\enspace\ignorespaces}%
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   860
 \setbox0=\vbox{\def\thanks##1{}\@institute}%
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   861
 \ifnum\c@@inst=1\relax
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   862
   \gdef\fnnstart{0}%
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   863
 \else
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   864
   \xdef\fnnstart{\c@@inst}%
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   865
   \setcounter{@inst}{1}%
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   866
   \noindent$^{\the@inst}$\enspace
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   867
 \fi
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   868
 \ignorespaces
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   869
 \@institute\par
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   870
 \endgroup}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   871
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   872
\def\@fnsymbol#1{\ensuremath{\ifcase#1\or\star\or{\star\star}\or
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   873
   {\star\star\star}\or \dagger\or \ddagger\or
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   874
   \mathchar "278\or \mathchar "27B\or \|\or **\or \dagger\dagger
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   875
   \or \ddagger\ddagger \else\@ctrerr\fi}}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   876
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   877
\def\inst#1{\unskip$^{#1}$}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   878
\def\fnmsep{\unskip$^,$}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   879
\def\email#1{{\tt#1}}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   880
\AtBeginDocument{\@ifundefined{url}{\def\url#1{#1}}{}%
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   881
\@ifpackageloaded{babel}{%
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   882
\@ifundefined{extrasenglish}{}{\addto\extrasenglish{\switcht@albion}}%
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   883
\@ifundefined{extrasfrenchb}{}{\addto\extrasfrenchb{\switcht@francais}}%
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   884
\@ifundefined{extrasgerman}{}{\addto\extrasgerman{\switcht@deutsch}}%
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   885
}{\switcht@@therlang}%
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   886
\providecommand{\keywords}[1]{\par\addvspace\baselineskip
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   887
\noindent\keywordname\enspace\ignorespaces#1}%
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   888
}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   889
\def\homedir{\~{ }}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   890
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   891
\def\subtitle#1{\gdef\@subtitle{#1}}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   892
\clearheadinfo
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   893
%
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   894
%%% to avoid hyperref warnings
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   895
\providecommand*{\toclevel@author}{999}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   896
%%% to make title-entry parent of section-entries
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   897
\providecommand*{\toclevel@title}{0}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   898
%
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   899
\renewcommand\maketitle{\newpage
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   900
\phantomsection
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   901
  \refstepcounter{chapter}%
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   902
  \stepcounter{section}%
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   903
  \setcounter{section}{0}%
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   904
  \setcounter{subsection}{0}%
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   905
  \setcounter{figure}{0}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   906
  \setcounter{table}{0}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   907
  \setcounter{equation}{0}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   908
  \setcounter{footnote}{0}%
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   909
  \begingroup
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   910
    \parindent=\z@
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   911
    \renewcommand\thefootnote{\@fnsymbol\c@footnote}%
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   912
    \if@twocolumn
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   913
      \ifnum \col@number=\@ne
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   914
        \@maketitle
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   915
      \else
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   916
        \twocolumn[\@maketitle]%
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   917
      \fi
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   918
    \else
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   919
      \newpage
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   920
      \global\@topnum\z@   % Prevents figures from going at top of page.
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   921
      \@maketitle
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   922
    \fi
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   923
    \thispagestyle{empty}\@thanks
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   924
%
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   925
    \def\\{\unskip\ \ignorespaces}\def\inst##1{\unskip{}}%
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   926
    \def\thanks##1{\unskip{}}\def\fnmsep{\unskip}%
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   927
    \instindent=\hsize
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   928
    \advance\instindent by-\headlineindent
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   929
    \if!\the\toctitle!\addcontentsline{toc}{title}{\@title}\else
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   930
       \addcontentsline{toc}{title}{\the\toctitle}\fi
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   931
    \if@runhead
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   932
       \if!\the\titlerunning!\else
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   933
         \edef\@title{\the\titlerunning}%
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   934
       \fi
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   935
       \global\setbox\titrun=\hbox{\small\rm\unboldmath\ignorespaces\@title}%
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   936
       \ifdim\wd\titrun>\instindent
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   937
          \typeout{Title too long for running head. Please supply}%
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   938
          \typeout{a shorter form with \string\titlerunning\space prior to
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   939
                   \string\maketitle}%
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   940
          \global\setbox\titrun=\hbox{\small\rm
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   941
          Title Suppressed Due to Excessive Length}%
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   942
       \fi
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   943
       \xdef\@title{\copy\titrun}%
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   944
    \fi
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   945
%
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   946
    \if!\the\tocauthor!\relax
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   947
      {\def\and{\noexpand\protect\noexpand\and}%
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   948
      \protected@xdef\toc@uthor{\@author}}%
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   949
    \else
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   950
      \def\\{\noexpand\protect\noexpand\newline}%
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   951
      \protected@xdef\scratch{\the\tocauthor}%
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   952
      \protected@xdef\toc@uthor{\scratch}%
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   953
    \fi
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   954
    \addtocontents{toc}{\noexpand\protect\noexpand\authcount{\the\c@auco}}%
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   955
    \addcontentsline{toc}{author}{\toc@uthor}%
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   956
    \if@runhead
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   957
       \if!\the\authorrunning!
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   958
         \value{@inst}=\value{@auth}%
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   959
         \setcounter{@auth}{1}%
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   960
       \else
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   961
         \edef\@author{\the\authorrunning}%
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   962
       \fi
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   963
       \global\setbox\authrun=\hbox{\small\unboldmath\@author\unskip}%
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   964
       \ifdim\wd\authrun>\instindent
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   965
          \typeout{Names of authors too long for running head. Please supply}%
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   966
          \typeout{a shorter form with \string\authorrunning\space prior to
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   967
                   \string\maketitle}%
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   968
          \global\setbox\authrun=\hbox{\small\rm
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   969
          Authors Suppressed Due to Excessive Length}%
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   970
       \fi
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   971
       \xdef\@author{\copy\authrun}%
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   972
       \markboth{\@author}{\@title}%
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   973
     \fi
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   974
  \endgroup
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   975
  \setcounter{footnote}{\fnnstart}%
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   976
  \clearheadinfo}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   977
%
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   978
\def\@maketitle{\newpage
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   979
 \markboth{}{}%
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   980
 \def\lastand{\ifnum\value{@inst}=2\relax
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   981
                 \unskip{} \andname\
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   982
              \else
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   983
                 \unskip \lastandname\
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   984
              \fi}%
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   985
 \def\and{\stepcounter{@auth}\relax
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   986
          \ifnum\value{@auth}=\value{@inst}%
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   987
             \lastand
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   988
          \else
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   989
             \unskip,
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   990
          \fi}%
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   991
 \begin{center}%
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   992
 \let\newline\\
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   993
 {\Large \bfseries\boldmath
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   994
  \pretolerance=10000
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   995
  \@title \par}\vskip .8cm
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   996
\if!\@subtitle!\else {\large \bfseries\boldmath
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   997
  \vskip -.65cm
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   998
  \pretolerance=10000
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   999
  \@subtitle \par}\vskip .8cm\fi
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1000
 \setbox0=\vbox{\setcounter{@auth}{1}\def\and{\stepcounter{@auth}}%
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1001
 \def\thanks##1{}\@author}%
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1002
 \global\value{@inst}=\value{@auth}%
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1003
 \global\value{auco}=\value{@auth}%
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1004
 \setcounter{@auth}{1}%
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1005
{\lineskip .5em
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1006
\noindent\ignorespaces
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1007
\@author\vskip.35cm}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1008
 {\small\institutename}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1009
 \end{center}%
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1010
 }
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1011
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1012
% definition of the "\spnewtheorem" command.
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1013
%
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1014
% Usage:
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1015
%
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1016
%     \spnewtheorem{env_nam}{caption}[within]{cap_font}{body_font}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1017
% or  \spnewtheorem{env_nam}[numbered_like]{caption}{cap_font}{body_font}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1018
% or  \spnewtheorem*{env_nam}{caption}{cap_font}{body_font}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1019
%
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1020
% New is "cap_font" and "body_font". It stands for
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1021
% fontdefinition of the caption and the text itself.
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1022
%
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1023
% "\spnewtheorem*" gives a theorem without number.
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1024
%
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1025
% A defined spnewthoerem environment is used as described
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1026
% by Lamport.
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1027
%
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1028
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1029
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1030
\def\@thmcountersep{}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1031
\def\@thmcounterend{.}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1032
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1033
\def\spnewtheorem{\@ifstar{\@sthm}{\@Sthm}}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1034
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1035
% definition of \spnewtheorem with number
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1036
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1037
\def\@spnthm#1#2{%
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1038
  \@ifnextchar[{\@spxnthm{#1}{#2}}{\@spynthm{#1}{#2}}}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1039
\def\@Sthm#1{\@ifnextchar[{\@spothm{#1}}{\@spnthm{#1}}}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1040
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1041
\def\@spxnthm#1#2[#3]#4#5{\expandafter\@ifdefinable\csname #1\endcsname
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1042
   {\@definecounter{#1}\@addtoreset{#1}{#3}%
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1043
   \expandafter\xdef\csname the#1\endcsname{\expandafter\noexpand
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1044
     \csname the#3\endcsname \noexpand\@thmcountersep \@thmcounter{#1}}%
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1045
   \expandafter\xdef\csname #1name\endcsname{#2}%
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1046
   \global\@namedef{#1}{\@spthm{#1}{\csname #1name\endcsname}{#4}{#5}}%
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1047
                              \global\@namedef{end#1}{\@endtheorem}}}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1048
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1049
\def\@spynthm#1#2#3#4{\expandafter\@ifdefinable\csname #1\endcsname
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1050
   {\@definecounter{#1}%
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1051
   \expandafter\xdef\csname the#1\endcsname{\@thmcounter{#1}}%
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1052
   \expandafter\xdef\csname #1name\endcsname{#2}%
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1053
   \global\@namedef{#1}{\@spthm{#1}{\csname #1name\endcsname}{#3}{#4}}%
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1054
                               \global\@namedef{end#1}{\@endtheorem}}}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1055
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1056
\def\@spothm#1[#2]#3#4#5{%
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1057
  \@ifundefined{c@#2}{\@latexerr{No theorem environment `#2' defined}\@eha}%
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1058
  {\expandafter\@ifdefinable\csname #1\endcsname
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1059
  {\newaliascnt{#1}{#2}%
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1060
  \expandafter\xdef\csname #1name\endcsname{#3}%
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1061
  \global\@namedef{#1}{\@spthm{#1}{\csname #1name\endcsname}{#4}{#5}}%
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1062
  \global\@namedef{end#1}{\@endtheorem}}}}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1063
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1064
\def\@spthm#1#2#3#4{\topsep 7\p@ \@plus2\p@ \@minus4\p@
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1065
\refstepcounter{#1}%
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1066
\@ifnextchar[{\@spythm{#1}{#2}{#3}{#4}}{\@spxthm{#1}{#2}{#3}{#4}}}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1067
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1068
\def\@spxthm#1#2#3#4{\@spbegintheorem{#2}{\csname the#1\endcsname}{#3}{#4}%
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1069
                    \ignorespaces}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1070
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1071
\def\@spythm#1#2#3#4[#5]{\@spopargbegintheorem{#2}{\csname
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1072
       the#1\endcsname}{#5}{#3}{#4}\ignorespaces}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1073
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1074
\def\@spbegintheorem#1#2#3#4{\trivlist
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1075
                 \item[\hskip\labelsep{#3#1\ #2\@thmcounterend}]#4}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1076
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1077
\def\@spopargbegintheorem#1#2#3#4#5{\trivlist
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1078
      \item[\hskip\labelsep{#4#1\ #2}]{#4(#3)\@thmcounterend\ }#5}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1079
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1080
% definition of \spnewtheorem* without number
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1081
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1082
\def\@sthm#1#2{\@Ynthm{#1}{#2}}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1083
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1084
\def\@Ynthm#1#2#3#4{\expandafter\@ifdefinable\csname #1\endcsname
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1085
   {\global\@namedef{#1}{\@Thm{\csname #1name\endcsname}{#3}{#4}}%
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1086
    \expandafter\xdef\csname #1name\endcsname{#2}%
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1087
    \global\@namedef{end#1}{\@endtheorem}}}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1088
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1089
\def\@Thm#1#2#3{\topsep 7\p@ \@plus2\p@ \@minus4\p@
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1090
\@ifnextchar[{\@Ythm{#1}{#2}{#3}}{\@Xthm{#1}{#2}{#3}}}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1091
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1092
\def\@Xthm#1#2#3{\@Begintheorem{#1}{#2}{#3}\ignorespaces}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1093
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1094
\def\@Ythm#1#2#3[#4]{\@Opargbegintheorem{#1}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1095
       {#4}{#2}{#3}\ignorespaces}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1096
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1097
\def\@Begintheorem#1#2#3{#3\trivlist
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1098
                           \item[\hskip\labelsep{#2#1\@thmcounterend}]}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1099
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1100
\def\@Opargbegintheorem#1#2#3#4{#4\trivlist
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1101
      \item[\hskip\labelsep{#3#1}]{#3(#2)\@thmcounterend\ }}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1102
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1103
\if@envcntsect
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1104
   \def\@thmcountersep{.}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1105
   \spnewtheorem{theorem}{Theorem}[section]{\bfseries}{\itshape}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1106
\else
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1107
   \spnewtheorem{theorem}{Theorem}{\bfseries}{\itshape}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1108
   \if@envcntreset
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1109
      \@addtoreset{theorem}{section}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1110
   \else
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1111
      \@addtoreset{theorem}{chapter}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1112
   \fi
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1113
\fi
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1114
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1115
%definition of divers theorem environments
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1116
\spnewtheorem*{claim}{Claim}{\itshape}{\rmfamily}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1117
\spnewtheorem*{proof}{Proof}{\itshape}{\rmfamily}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1118
\if@envcntsame % alle Umgebungen wie Theorem.
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1119
   \def\spn@wtheorem#1#2#3#4{\@spothm{#1}[theorem]{#2}{#3}{#4}}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1120
\else % alle Umgebungen mit eigenem Zaehler
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1121
   \if@envcntsect % mit section numeriert
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1122
      \def\spn@wtheorem#1#2#3#4{\@spxnthm{#1}{#2}[section]{#3}{#4}}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1123
   \else % nicht mit section numeriert
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1124
      \if@envcntreset
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1125
         \def\spn@wtheorem#1#2#3#4{\@spynthm{#1}{#2}{#3}{#4}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1126
                                   \@addtoreset{#1}{section}}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1127
      \else
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1128
         \def\spn@wtheorem#1#2#3#4{\@spynthm{#1}{#2}{#3}{#4}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1129
                                   \@addtoreset{#1}{chapter}}%
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1130
      \fi
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1131
   \fi
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1132
\fi
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1133
\spn@wtheorem{case}{Case}{\itshape}{\rmfamily}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1134
\spn@wtheorem{conjecture}{Conjecture}{\itshape}{\rmfamily}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1135
\spn@wtheorem{corollary}{Corollary}{\bfseries}{\itshape}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1136
\spn@wtheorem{definition}{Definition}{\bfseries}{\itshape}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1137
\spn@wtheorem{example}{Example}{\itshape}{\rmfamily}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1138
\spn@wtheorem{exercise}{Exercise}{\itshape}{\rmfamily}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1139
\spn@wtheorem{lemma}{Lemma}{\bfseries}{\itshape}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1140
\spn@wtheorem{note}{Note}{\itshape}{\rmfamily}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1141
\spn@wtheorem{problem}{Problem}{\itshape}{\rmfamily}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1142
\spn@wtheorem{property}{Property}{\itshape}{\rmfamily}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1143
\spn@wtheorem{proposition}{Proposition}{\bfseries}{\itshape}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1144
\spn@wtheorem{question}{Question}{\itshape}{\rmfamily}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1145
\spn@wtheorem{solution}{Solution}{\itshape}{\rmfamily}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1146
\spn@wtheorem{remark}{Remark}{\itshape}{\rmfamily}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1147
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1148
\def\@takefromreset#1#2{%
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1149
    \def\@tempa{#1}%
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1150
    \let\@tempd\@elt
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1151
    \def\@elt##1{%
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1152
        \def\@tempb{##1}%
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1153
        \ifx\@tempa\@tempb\else
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1154
            \@addtoreset{##1}{#2}%
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1155
        \fi}%
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1156
    \expandafter\expandafter\let\expandafter\@tempc\csname cl@#2\endcsname
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1157
    \expandafter\def\csname cl@#2\endcsname{}%
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1158
    \@tempc
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1159
    \let\@elt\@tempd}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1160
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1161
\def\theopargself{\def\@spopargbegintheorem##1##2##3##4##5{\trivlist
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1162
      \item[\hskip\labelsep{##4##1\ ##2}]{##4##3\@thmcounterend\ }##5}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1163
                  \def\@Opargbegintheorem##1##2##3##4{##4\trivlist
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1164
      \item[\hskip\labelsep{##3##1}]{##3##2\@thmcounterend\ }}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1165
      }
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1166
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1167
\renewenvironment{abstract}{%
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1168
      \list{}{\advance\topsep by0.35cm\relax\small
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1169
      \leftmargin=1cm
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1170
      \labelwidth=\z@
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1171
      \listparindent=\z@
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1172
      \itemindent\listparindent
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1173
      \rightmargin\leftmargin}\item[\hskip\labelsep
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1174
                                    \bfseries\abstractname]}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1175
    {\endlist}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1176
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1177
\newdimen\headlineindent             % dimension for space between
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1178
\headlineindent=1.166cm              % number and text of headings.
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1179
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1180
\def\ps@headings{\let\@mkboth\@gobbletwo
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1181
   \let\@oddfoot\@empty\let\@evenfoot\@empty
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1182
   \def\@evenhead{\normalfont\small\rlap{\thepage}\hspace{\headlineindent}%
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1183
                  \leftmark\hfil}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1184
   \def\@oddhead{\normalfont\small\hfil\rightmark\hspace{\headlineindent}%
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1185
                 \llap{\thepage}}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1186
   \def\chaptermark##1{}%
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1187
   \def\sectionmark##1{}%
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1188
   \def\subsectionmark##1{}}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1189
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1190
\def\ps@titlepage{\let\@mkboth\@gobbletwo
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1191
   \let\@oddfoot\@empty\let\@evenfoot\@empty
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1192
   \def\@evenhead{\normalfont\small\rlap{\thepage}\hspace{\headlineindent}%
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1193
                  \hfil}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1194
   \def\@oddhead{\normalfont\small\hfil\hspace{\headlineindent}%
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1195
                 \llap{\thepage}}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1196
   \def\chaptermark##1{}%
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1197
   \def\sectionmark##1{}%
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1198
   \def\subsectionmark##1{}}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1199
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1200
\if@runhead\ps@headings\else
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1201
\ps@empty\fi
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1202
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1203
\setlength\arraycolsep{1.4\p@}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1204
\setlength\tabcolsep{1.4\p@}
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1205
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1206
\endinput
05ccb61aa628 started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1207
%end of file llncs.cls