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