Quotient-Paper/document/svjour3.cls
author Christian Urban <urbanc@in.tum.de>
Wed, 30 Mar 2011 22:27:26 +0200
changeset 2750 43283267737c
parent 1975 b1281a0051ae
permissions -rwxr-xr-x
more on the slides
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
1975
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
     1
% SVJour3 DOCUMENT CLASS -- version 3.2 for LaTeX2e
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
     2
%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
     3
% LaTeX document class for Springer journals
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
     4
%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
     5
%%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
     6
%%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
     7
%% \CharacterTable
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
     8
%%  {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
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
     9
%%   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
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    10
%%   Digits        \0\1\2\3\4\5\6\7\8\9
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    11
%%   Exclamation   \!     Double quote  \"     Hash (number) \#
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    12
%%   Dollar        \$     Percent       \%     Ampersand     \&
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    13
%%   Acute accent  \'     Left paren    \(     Right paren   \)
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    14
%%   Asterisk      \*     Plus          \+     Comma         \,
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    15
%%   Minus         \-     Point         \.     Solidus       \/
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    16
%%   Colon         \:     Semicolon     \;     Less than     \<
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    17
%%   Equals        \=     Greater than  \>     Question mark \?
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    18
%%   Commercial at \@     Left bracket  \[     Backslash     \\
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    19
%%   Right bracket \]     Circumflex    \^     Underscore    \_
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    20
%%   Grave accent  \`     Left brace    \{     Vertical bar  \|
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    21
%%   Right brace   \}     Tilde         \~}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    22
\NeedsTeXFormat{LaTeX2e}[1995/12/01]
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    23
\ProvidesClass{svjour3}[2007/05/08 v3.2
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    24
^^JLaTeX document class for Springer journals]
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    25
\newcommand\@ptsize{}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    26
\newif\if@restonecol
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    27
\newif\if@titlepage
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    28
\@titlepagefalse
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    29
\DeclareOption{a4paper}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    30
   {\setlength\paperheight {297mm}%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    31
    \setlength\paperwidth  {210mm}}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    32
\DeclareOption{10pt}{\renewcommand\@ptsize{0}}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    33
\DeclareOption{twoside}{\@twosidetrue  \@mparswitchtrue}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    34
\DeclareOption{draft}{\setlength\overfullrule{5pt}}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    35
\DeclareOption{final}{\setlength\overfullrule{0pt}}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    36
\DeclareOption{fleqn}{\input{fleqn.clo}\AtBeginDocument{\mathindent\z@}%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    37
\AtBeginDocument{\@ifpackageloaded{amsmath}{\@mathmargin\z@}{}}%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    38
\PassOptionsToPackage{fleqn}{amsmath}}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    39
%%%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    40
\DeclareOption{onecolumn}{}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    41
\DeclareOption{smallcondensed}{}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    42
\DeclareOption{twocolumn}{\@twocolumntrue\ExecuteOptions{fleqn}}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    43
\newif\if@smallext\@smallextfalse
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    44
\DeclareOption{smallextended}{\@smallexttrue}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    45
\let\if@mathematic\iftrue
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    46
\let\if@numbook\iffalse
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    47
\DeclareOption{numbook}{\let\if@envcntsect\iftrue
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    48
  \AtEndOfPackage{%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    49
   \renewcommand\thefigure{\thesection.\@arabic\c@figure}%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    50
   \renewcommand\thetable{\thesection.\@arabic\c@table}%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    51
   \renewcommand\theequation{\thesection.\@arabic\c@equation}%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    52
   \@addtoreset{figure}{section}%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    53
   \@addtoreset{table}{section}%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    54
   \@addtoreset{equation}{section}%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    55
  }%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    56
}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    57
\DeclareOption{openbib}{%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    58
  \AtEndOfPackage{%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    59
   \renewcommand\@openbib@code{%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    60
      \advance\leftmargin\bibindent
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    61
      \itemindent -\bibindent
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    62
      \listparindent \itemindent
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    63
      \parsep \z@
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    64
      }%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    65
   \renewcommand\newblock{\par}}%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    66
}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    67
\DeclareOption{natbib}{%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    68
\AtEndOfClass{\RequirePackage{natbib}%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    69
% Changing some parameters of NATBIB
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    70
\setlength{\bibhang}{\parindent}%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    71
%\setlength{\bibsep}{0mm}%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    72
\let\bibfont=\small
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    73
\def\@biblabel#1{#1.}%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    74
\newcommand{\etal}{et al.}%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    75
\bibpunct{(}{)}{;}{a}{}{,}}}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    76
%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    77
\let\if@runhead\iffalse
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    78
\DeclareOption{runningheads}{\let\if@runhead\iftrue}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    79
\let\if@smartrunh\iffalse
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    80
\DeclareOption{smartrunhead}{\let\if@smartrunh\iftrue}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    81
\DeclareOption{nosmartrunhead}{\let\if@smartrunh\iffalse}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    82
\let\if@envcntreset\iffalse
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    83
\DeclareOption{envcountreset}{\let\if@envcntreset\iftrue}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    84
\let\if@envcntsame\iffalse
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    85
\DeclareOption{envcountsame}{\let\if@envcntsame\iftrue}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    86
\let\if@envcntsect\iffalse
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    87
\DeclareOption{envcountsect}{\let\if@envcntsect\iftrue}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    88
\let\if@referee\iffalse
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    89
\DeclareOption{referee}{\let\if@referee\iftrue}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    90
\def\makereferee{\def\baselinestretch{2}}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    91
\let\if@instindent\iffalse
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    92
\DeclareOption{instindent}{\let\if@instindent\iftrue}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    93
\let\if@smartand\iffalse
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    94
\DeclareOption{smartand}{\let\if@smartand\iftrue}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    95
\let\if@spthms\iftrue
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    96
\DeclareOption{nospthms}{\let\if@spthms\iffalse}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    97
%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    98
% language and babel dependencies
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    99
\DeclareOption{deutsch}{\def\switcht@@therlang{\switcht@deutsch}%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   100
\gdef\svlanginfo{\typeout{Man spricht deutsch.}\global\let\svlanginfo\relax}}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   101
\DeclareOption{francais}{\def\switcht@@therlang{\switcht@francais}%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   102
\gdef\svlanginfo{\typeout{On parle francais.}\global\let\svlanginfo\relax}}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   103
\let\switcht@@therlang\relax
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   104
\let\svlanginfo\relax
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   105
%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   106
\AtBeginDocument{\@ifpackageloaded{babel}{%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   107
\@ifundefined{extrasenglish}{}{\addto\extrasenglish{\switcht@albion}}%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   108
\@ifundefined{extrasUKenglish}{}{\addto\extrasUKenglish{\switcht@albion}}%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   109
\@ifundefined{extrasfrenchb}{}{\addto\extrasfrenchb{\switcht@francais}}%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   110
\@ifundefined{extrasgerman}{}{\addto\extrasgerman{\switcht@deutsch}}%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   111
\@ifundefined{extrasngerman}{}{\addto\extrasngerman{\switcht@deutsch}}%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   112
}{\switcht@@therlang}%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   113
}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   114
%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   115
\def\ClassInfoNoLine#1#2{%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   116
   \ClassInfo{#1}{#2\@gobble}%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   117
}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   118
\let\journalopt\@empty
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   119
\DeclareOption*{%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   120
\InputIfFileExists{sv\CurrentOption.clo}{%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   121
\global\let\journalopt\CurrentOption}{%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   122
\ClassWarning{Springer-SVJour3}{Specified option or subpackage
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   123
"\CurrentOption" not found -}\OptionNotUsed}}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   124
\ExecuteOptions{a4paper,twoside,10pt,instindent}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   125
\ProcessOptions
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   126
%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   127
\ifx\journalopt\@empty\relax
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   128
\ClassInfoNoLine{Springer-SVJour3}{extra/valid Springer sub-package (-> *.clo)
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   129
\MessageBreak not found in option list of \string\documentclass
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   130
\MessageBreak  - autoactivating "global" style}{}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   131
\input{svglov3.clo}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   132
\else
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   133
\@ifundefined{validfor}{%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   134
\ClassError{Springer-SVJour3}{Possible option clash for sub-package
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   135
\MessageBreak "sv\journalopt.clo" - option file not valid
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   136
\MessageBreak for this class}{Perhaps you used an option of the old
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   137
Springer class SVJour!}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   138
}{}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   139
\fi
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   140
%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   141
\if@smartrunh\AtEndDocument{\islastpageeven\getlastpagenumber}\fi
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   142
%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   143
\newcommand{\twocoltest}[2]{\if@twocolumn\def\@gtempa{#2}\else\def\@gtempa{#1}\fi
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   144
\@gtempa\makeatother}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   145
\newcommand{\columncase}{\makeatletter\twocoltest}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   146
%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   147
\DeclareMathSymbol{\Gamma}{\mathalpha}{letters}{"00}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   148
\DeclareMathSymbol{\Delta}{\mathalpha}{letters}{"01}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   149
\DeclareMathSymbol{\Theta}{\mathalpha}{letters}{"02}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   150
\DeclareMathSymbol{\Lambda}{\mathalpha}{letters}{"03}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   151
\DeclareMathSymbol{\Xi}{\mathalpha}{letters}{"04}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   152
\DeclareMathSymbol{\Pi}{\mathalpha}{letters}{"05}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   153
\DeclareMathSymbol{\Sigma}{\mathalpha}{letters}{"06}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   154
\DeclareMathSymbol{\Upsilon}{\mathalpha}{letters}{"07}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   155
\DeclareMathSymbol{\Phi}{\mathalpha}{letters}{"08}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   156
\DeclareMathSymbol{\Psi}{\mathalpha}{letters}{"09}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   157
\DeclareMathSymbol{\Omega}{\mathalpha}{letters}{"0A}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   158
%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   159
\setlength\parindent{15\p@}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   160
\setlength\smallskipamount{3\p@ \@plus 1\p@ \@minus 1\p@}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   161
\setlength\medskipamount{6\p@ \@plus 2\p@ \@minus 2\p@}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   162
\setlength\bigskipamount{12\p@ \@plus 4\p@ \@minus 4\p@}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   163
\setlength\headheight{12\p@}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   164
\setlength\headsep   {14.50dd}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   165
\setlength\topskip   {10\p@}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   166
\setlength\footskip{30\p@}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   167
\setlength\maxdepth{.5\topskip}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   168
%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   169
\@settopoint\textwidth
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   170
\setlength\marginparsep {10\p@}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   171
\setlength\marginparpush{5\p@}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   172
\setlength\topmargin{-10pt}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   173
\if@twocolumn
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   174
   \setlength\oddsidemargin {-30\p@}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   175
   \setlength\evensidemargin{-30\p@}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   176
\else
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   177
   \setlength\oddsidemargin {\z@}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   178
   \setlength\evensidemargin{\z@}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   179
\fi
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   180
\setlength\marginparwidth  {48\p@}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   181
\setlength\footnotesep{8\p@}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   182
\setlength{\skip\footins}{9\p@ \@plus 4\p@ \@minus 2\p@}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   183
\setlength\floatsep    {12\p@ \@plus 2\p@ \@minus 2\p@}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   184
\setlength\textfloatsep{20\p@ \@plus 2\p@ \@minus 4\p@}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   185
\setlength\intextsep   {20\p@ \@plus 2\p@ \@minus 2\p@}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   186
\setlength\dblfloatsep    {12\p@ \@plus 2\p@ \@minus 2\p@}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   187
\setlength\dbltextfloatsep{20\p@ \@plus 2\p@ \@minus 4\p@}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   188
\setlength\@fptop{0\p@}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   189
\setlength\@fpsep{12\p@ \@plus 2\p@ \@minus 2\p@}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   190
\setlength\@fpbot{0\p@ \@plus 1fil}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   191
\setlength\@dblfptop{0\p@}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   192
\setlength\@dblfpsep{12\p@ \@plus 2\p@ \@minus 2\p@}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   193
\setlength\@dblfpbot{0\p@ \@plus 1fil}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   194
\setlength\partopsep{2\p@ \@plus 1\p@ \@minus 1\p@}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   195
\def\@listi{\leftmargin\leftmargini
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   196
            \parsep \z@
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   197
            \topsep 6\p@ \@plus2\p@ \@minus4\p@
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   198
            \itemsep\parsep}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   199
\let\@listI\@listi
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   200
\@listi
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   201
\def\@listii {\leftmargin\leftmarginii
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   202
              \labelwidth\leftmarginii
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   203
              \advance\labelwidth-\labelsep
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   204
              \topsep    \z@
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   205
              \parsep    \topsep
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   206
              \itemsep   \parsep}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   207
\def\@listiii{\leftmargin\leftmarginiii
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   208
              \labelwidth\leftmarginiii
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   209
              \advance\labelwidth-\labelsep
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   210
              \topsep    \z@
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   211
              \parsep    \topsep
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   212
              \itemsep   \parsep}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   213
\def\@listiv {\leftmargin\leftmarginiv
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   214
              \labelwidth\leftmarginiv
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   215
              \advance\labelwidth-\labelsep}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   216
\def\@listv  {\leftmargin\leftmarginv
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   217
              \labelwidth\leftmarginv
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   218
              \advance\labelwidth-\labelsep}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   219
\def\@listvi {\leftmargin\leftmarginvi
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   220
              \labelwidth\leftmarginvi
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   221
              \advance\labelwidth-\labelsep}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   222
%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   223
\setlength\lineskip{1\p@}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   224
\setlength\normallineskip{1\p@}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   225
\renewcommand\baselinestretch{}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   226
\setlength\parskip{0\p@ \@plus \p@}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   227
\@lowpenalty   51
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   228
\@medpenalty  151
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   229
\@highpenalty 301
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   230
\setcounter{topnumber}{4}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   231
\renewcommand\topfraction{.9}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   232
\setcounter{bottomnumber}{2}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   233
\renewcommand\bottomfraction{.7}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   234
\setcounter{totalnumber}{6}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   235
\renewcommand\textfraction{.1}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   236
\renewcommand\floatpagefraction{.85}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   237
\setcounter{dbltopnumber}{3}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   238
\renewcommand\dbltopfraction{.85}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   239
\renewcommand\dblfloatpagefraction{.85}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   240
\def\ps@headings{%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   241
    \let\@oddfoot\@empty\let\@evenfoot\@empty
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   242
    \def\@evenhead{\small\csname runheadhook\endcsname
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   243
    \rlap{\thepage}\hfil\leftmark\unskip}%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   244
    \def\@oddhead{\small\csname runheadhook\endcsname
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   245
    \ignorespaces\rightmark\hfil\llap{\thepage}}%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   246
    \let\@mkboth\@gobbletwo
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   247
    \let\sectionmark\@gobble
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   248
    \let\subsectionmark\@gobble
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   249
    }
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   250
% make indentations changeable
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   251
\def\setitemindent#1{\settowidth{\labelwidth}{#1}%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   252
        \leftmargini\labelwidth
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   253
        \advance\leftmargini\labelsep
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   254
   \def\@listi{\leftmargin\leftmargini
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   255
        \labelwidth\leftmargini\advance\labelwidth by -\labelsep
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   256
        \parsep=\parskip
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   257
        \topsep=\medskipamount
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   258
        \itemsep=\parskip \advance\itemsep by -\parsep}}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   259
\def\setitemitemindent#1{\settowidth{\labelwidth}{#1}%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   260
        \leftmarginii\labelwidth
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   261
        \advance\leftmarginii\labelsep
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   262
\def\@listii{\leftmargin\leftmarginii
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   263
        \labelwidth\leftmarginii\advance\labelwidth by -\labelsep
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   264
        \parsep=\parskip
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   265
        \topsep=\z@
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   266
        \itemsep=\parskip \advance\itemsep by -\parsep}}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   267
% labels of description
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   268
\def\descriptionlabel#1{\hspace\labelsep #1\hfil}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   269
% adjusted environment "description"
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   270
% if an optional parameter (at the first two levels of lists)
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   271
% is present, its width is considered to be the widest mark
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   272
% throughout the current list.
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   273
\def\description{\@ifnextchar[{\@describe}{\list{}{\labelwidth\z@
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   274
          \itemindent-\leftmargin \let\makelabel\descriptionlabel}}}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   275
\let\enddescription\endlist
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   276
%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   277
\def\describelabel#1{#1\hfil}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   278
\def\@describe[#1]{\relax\ifnum\@listdepth=0
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   279
\setitemindent{#1}\else\ifnum\@listdepth=1
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   280
\setitemitemindent{#1}\fi\fi
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   281
\list{--}{\let\makelabel\describelabel}}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   282
%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   283
\newdimen\logodepth
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   284
\logodepth=1.2cm
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   285
\newdimen\headerboxheight
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   286
\headerboxheight=163pt % 18 10.5dd-lines - 2\baselineskip
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   287
\if@twocolumn\else\advance\headerboxheight by-14.5mm\fi
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   288
\newdimen\betweenumberspace          % dimension for space between
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   289
\betweenumberspace=3.33pt            % number and text of titles.
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   290
\newdimen\aftertext                  % dimension for space after
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   291
\aftertext=5pt                       % text of title.
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   292
\newdimen\headlineindent             % dimension for space between
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   293
\headlineindent=1.166cm              % number and text of headings.
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   294
\if@mathematic
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   295
   \def\runinend{} % \enspace}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   296
   \def\floatcounterend{\enspace}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   297
   \def\sectcounterend{}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   298
\else
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   299
   \def\runinend{.}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   300
   \def\floatcounterend{.\ }
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   301
   \def\sectcounterend{.}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   302
\fi
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   303
\def\email#1{\emailname: #1}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   304
\def\keywords#1{\par\addvspace\medskipamount{\rightskip=0pt plus1cm
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   305
\def\and{\ifhmode\unskip\nobreak\fi\ $\cdot$
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   306
}\noindent\keywordname\enspace\ignorespaces#1\par}}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   307
%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   308
\def\subclassname{{\bfseries Mathematics Subject Classification
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   309
(2000)}\enspace}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   310
\def\subclass#1{\par\addvspace\medskipamount{\rightskip=0pt plus1cm
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   311
\def\and{\ifhmode\unskip\nobreak\fi\ $\cdot$
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   312
}\noindent\subclassname\ignorespaces#1\par}}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   313
%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   314
\def\PACSname{\textbf{PACS}\enspace}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   315
\def\PACS#1{\par\addvspace\medskipamount{\rightskip=0pt plus1cm
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   316
\def\and{\ifhmode\unskip\nobreak\fi\ $\cdot$
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   317
}\noindent\PACSname\ignorespaces#1\par}}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   318
%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   319
\def\CRclassname{{\bfseries CR Subject Classification}\enspace}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   320
\def\CRclass#1{\par\addvspace\medskipamount{\rightskip=0pt plus1cm
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   321
\def\and{\ifhmode\unskip\nobreak\fi\ $\cdot$
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   322
}\noindent\CRclassname\ignorespaces#1\par}}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   323
%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   324
\def\ESMname{\textbf{Electronic Supplementary Material}\enspace}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   325
\def\ESM#1{\par\addvspace\medskipamount
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   326
\noindent\ESMname\ignorespaces#1\par}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   327
%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   328
\newcounter{inst}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   329
\newcounter{auth}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   330
\def\authdepth{2}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   331
\newdimen\instindent
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   332
\newbox\authrun
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   333
\newtoks\authorrunning
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   334
\newbox\titrun
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   335
\newtoks\titlerunning
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   336
\def\authorfont{\bfseries}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   337
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   338
\def\combirunning#1{\gdef\@combi{#1}}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   339
\def\@combi{}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   340
\newbox\combirun
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   341
%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   342
\def\ps@last{\def\@evenhead{\small\rlap{\thepage}\hfil
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   343
\lastevenhead}}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   344
\newcounter{lastpage}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   345
\def\islastpageeven{\@ifundefined{lastpagenumber}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   346
{\setcounter{lastpage}{0}}{\setcounter{lastpage}{\lastpagenumber}}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   347
\ifnum\value{lastpage}>0
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   348
   \ifodd\value{lastpage}%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   349
   \else
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   350
      \if@smartrunh
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   351
         \thispagestyle{last}%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   352
      \fi
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   353
   \fi
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   354
\fi}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   355
\def\getlastpagenumber{\clearpage
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   356
\addtocounter{page}{-1}%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   357
   \immediate\write\@auxout{\string\gdef\string\lastpagenumber{\thepage}}%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   358
   \immediate\write\@auxout{\string\newlabel{LastPage}{{}{\thepage}}}%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   359
   \addtocounter{page}{1}}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   360
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   361
\def\journalname#1{\gdef\@journalname{#1}}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   362
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   363
\def\dedication#1{\gdef\@dedic{#1}}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   364
\def\@dedic{}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   365
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   366
\let\@date\undefined
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   367
\def\notused{~}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   368
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   369
\def\institute#1{\gdef\@institute{#1}}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   370
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   371
\def\offprints#1{\begingroup
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   372
\def\protect{\noexpand\protect\noexpand}\xdef\@thanks{\@thanks
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   373
\protect\footnotetext[0]{\unskip\hskip-15pt{\itshape Send offprint requests
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   374
to\/}: \ignorespaces#1}}\endgroup\ignorespaces}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   375
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   376
%\def\mail#1{\gdef\@mail{#1}}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   377
%\def\@mail{}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   378
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   379
\def\@thanks{}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   380
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   381
\def\@fnsymbol#1{\ifcase#1\or\star\or{\star\star}\or{\star\star\star}%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   382
   \or \dagger\or \ddagger\or
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   383
   \mathchar "278\or \mathchar "27B\or \|\or **\or \dagger\dagger
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   384
   \or \ddagger\ddagger \else\@ctrerr\fi\relax}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   385
%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   386
%\def\invthanks#1{\footnotetext[0]{\kern-\bibindent#1}}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   387
%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   388
\def\nothanksmarks{\def\thanks##1{\protected@xdef\@thanks{\@thanks
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   389
        \protect\footnotetext[0]{\kern-\bibindent##1}}}}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   390
%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   391
\def\subtitle#1{\gdef\@subtitle{#1}}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   392
\def\@subtitle{}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   393
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   394
\def\headnote#1{\gdef\@headnote{#1}}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   395
\def\@headnote{}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   396
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   397
\def\papertype#1{\gdef\paper@type{\MakeUppercase{#1}}}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   398
\def\paper@type{}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   399
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   400
\def\ch@ckobl#1#2{\@ifundefined{@#1}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   401
 {\typeout{SVJour3 warning: Missing
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   402
\expandafter\string\csname#1\endcsname}%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   403
  \csname #1\endcsname{#2}}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   404
 {}}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   405
%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   406
\def\ProcessRunnHead{%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   407
    \def\\{\unskip\ \ignorespaces}%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   408
    \def\thanks##1{\unskip{}}%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   409
    \instindent=\textwidth
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   410
    \advance\instindent by-\headlineindent
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   411
    \if!\the\titlerunning!\else
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   412
      \edef\@title{\the\titlerunning}%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   413
    \fi
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   414
    \global\setbox\titrun=\hbox{\small\rmfamily\unboldmath\ignorespaces\@title
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   415
                                \unskip}%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   416
    \ifdim\wd\titrun>\instindent
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   417
       \typeout{^^JSVJour3 Warning: Title too long for running head.}%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   418
       \typeout{Please supply a shorter form with \string\titlerunning
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   419
                \space prior to \string\maketitle}%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   420
       \global\setbox\titrun=\hbox{\small\rmfamily
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   421
       Title Suppressed Due to Excessive Length}%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   422
    \fi
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   423
    \xdef\@title{\copy\titrun}%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   424
%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   425
    \if!\the\authorrunning!
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   426
    \else
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   427
      \setcounter{auth}{1}%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   428
      \edef\@author{\the\authorrunning}%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   429
    \fi
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   430
    \ifnum\value{inst}>\authdepth
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   431
       \def\stripauthor##1\and##2\endauthor{%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   432
       \protected@xdef\@author{##1\unskip\unskip\if!##2!\else\ et al.\fi}}%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   433
       \expandafter\stripauthor\@author\and\endauthor
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   434
    \else
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   435
       \gdef\and{\unskip, \ignorespaces}%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   436
       {\def\and{\noexpand\protect\noexpand\and}%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   437
       \protected@xdef\@author{\@author}}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   438
    \fi
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   439
    \global\setbox\authrun=\hbox{\small\rmfamily\unboldmath\ignorespaces
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   440
                                 \@author\unskip}%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   441
    \ifdim\wd\authrun>\instindent
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   442
    \typeout{^^JSVJour3 Warning: Author name(s) too long for running head.
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   443
             ^^JPlease supply a shorter form with \string\authorrunning
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   444
             \space prior to \string\maketitle}%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   445
    \global\setbox\authrun=\hbox{\small\rmfamily Please give a shorter version
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   446
          with: {\tt\string\authorrunning\space and
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   447
             \string\titlerunning\space prior to \string\maketitle}}%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   448
    \fi
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   449
    \xdef\@author{\copy\authrun}%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   450
    \markboth{\@author}{\@title}%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   451
}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   452
%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   453
\let\orithanks=\thanks
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   454
\def\thanks#1{\ClassWarning{SVJour3}{\string\thanks\space may only be
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   455
used inside of \string\title, \string\author,\MessageBreak
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   456
and \string\date\space prior to \string\maketitle}}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   457
%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   458
\def\maketitle{\par\let\thanks=\orithanks
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   459
\ch@ckobl{}{Noname}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   460
\ch@ckobl{date}{the date of receipt and acceptance should be inserted
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   461
later}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   462
\ch@ckobl{title}{A title should be given}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   463
\ch@ckobl{author}{Name(s) and initial(s) of author(s) should be given}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   464
\ch@ckobl{institute}{Address(es) of author(s) should be given}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   465
\begingroup
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   466
%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   467
    \renewcommand\thefootnote{\@fnsymbol\c@footnote}%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   468
    \def\@makefnmark{$^{\@thefnmark}$}%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   469
    \renewcommand\@makefntext[1]{%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   470
    \noindent
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   471
    \hb@xt@\bibindent{\hss\@makefnmark\enspace}##1\vrule height0pt
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   472
    width0pt depth8pt}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   473
%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   474
 \def\lastand{\ifnum\value{inst}=2\relax
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   475
                 \unskip{} \andname\
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   476
              \else
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   477
                 \unskip, \andname\
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   478
              \fi}%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   479
 \def\and{\stepcounter{auth}\relax
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   480
          \if@smartand
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   481
             \ifnum\value{auth}=\value{inst}%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   482
                \lastand
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   483
             \else
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   484
                \unskip,
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   485
             \fi
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   486
          \else
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   487
             \unskip,
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   488
          \fi}%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   489
 \thispagestyle{empty}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   490
 \ifnum \col@number=\@ne
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   491
   \@maketitle
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   492
 \else
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   493
   \twocolumn[\@maketitle]%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   494
 \fi
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   495
%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   496
 \global\@topnum\z@
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   497
 \if!\@thanks!\else
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   498
    \@thanks
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   499
\insert\footins{\vskip-3pt\hrule\@width\if@twocolumn\columnwidth
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   500
\else 38mm\fi\vskip3pt}%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   501
 \fi
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   502
 {\def\thanks##1{\unskip{}}%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   503
 \def\iand{\\[5pt]\let\and=\nand}%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   504
 \def\nand{\ifhmode\unskip\nobreak\fi\ $\cdot$ }%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   505
 \let\and=\nand
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   506
 \def\at{\\\let\and=\iand}%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   507
 \footnotetext[0]{\kern-\bibindent
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   508
 \ignorespaces\@institute}\vspace{5dd}}%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   509
%\if!\@mail!\else
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   510
%   \footnotetext[0]{\kern-\bibindent\mailname\
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   511
%   \ignorespaces\@mail}%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   512
%\fi
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   513
%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   514
 \if@runhead
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   515
    \ProcessRunnHead
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   516
 \fi
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   517
%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   518
 \endgroup
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   519
 \setcounter{footnote}{0}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   520
 \global\let\thanks\relax
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   521
 \global\let\maketitle\relax
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   522
 \global\let\@maketitle\relax
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   523
 \global\let\@thanks\@empty
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   524
 \global\let\@author\@empty
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   525
 \global\let\@date\@empty
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   526
 \global\let\@title\@empty
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   527
 \global\let\@subtitle\@empty
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   528
 \global\let\title\relax
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   529
 \global\let\author\relax
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   530
 \global\let\date\relax
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   531
 \global\let\and\relax}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   532
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   533
\def\makeheadbox{{%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   534
\hbox to0pt{\vbox{\baselineskip=10dd\hrule\hbox
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   535
to\hsize{\vrule\kern3pt\vbox{\kern3pt
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   536
\hbox{J Automated Reasoning}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   537
\hbox{}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   538
\kern3pt}\hfil\kern3pt\vrule}\hrule}%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   539
\hss}}}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   540
%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   541
\def\rubric{\setbox0=\hbox{\small\strut}\@tempdima=\ht0\advance
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   542
\@tempdima\dp0\advance\@tempdima2\fboxsep\vrule\@height\@tempdima
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   543
\@width\z@}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   544
\newdimen\rubricwidth
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   545
%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   546
\def\@maketitle{\newpage
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   547
\normalfont
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   548
\vbox to0pt{\if@twocolumn\vskip-39pt\else\vskip-49pt\fi
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   549
\nointerlineskip
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   550
\makeheadbox\vss}\nointerlineskip
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   551
\vbox to 0pt{\offinterlineskip\rubricwidth=\columnwidth
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   552
%%%%\vskip-12.5pt          % -12.5pt
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   553
\if@twocolumn\else % one column journal
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   554
   \divide\rubricwidth by144\multiply\rubricwidth by89 % perform golden section
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   555
   \vskip-\topskip
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   556
\fi
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   557
\hrule\@height0.35mm\noindent
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   558
\advance\fboxsep by.25mm
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   559
\global\advance\rubricwidth by0pt
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   560
\rubric
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   561
\vss}\vskip19.5pt    % war 9pt
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   562
%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   563
\if@twocolumn\else
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   564
 \gdef\footnoterule{%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   565
  \kern-3\p@
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   566
  \hrule\@width38mm     % \columnwidth  \rubricwidth
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   567
  \kern2.6\p@}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   568
\fi
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   569
%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   570
 \setbox\authrun=\vbox\bgroup
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   571
     \if@twocolumn
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   572
        \hrule\@height10.5mm\@width0\p@
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   573
     \else
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   574
        \hrule\@height 2mm\@width0\p@
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   575
     \fi
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   576
     \pretolerance=10000
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   577
     \rightskip=0pt plus 4cm
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   578
    \nothanksmarks
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   579
%   \if!\@headnote!\else
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   580
%     \noindent
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   581
%     {\LARGE\normalfont\itshape\ignorespaces\@headnote\par}\vskip 3.5mm
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   582
%   \fi
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   583
    {\LARGE\bfseries
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   584
     \noindent\ignorespaces
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   585
     \@title \par}\vskip 17pt\relax
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   586
    \if!\@subtitle!\else
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   587
      {\large\bfseries
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   588
      \pretolerance=10000
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   589
      \rightskip=0pt plus 3cm
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   590
      \vskip-12pt
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   591
%     \noindent\ignorespaces\@subtitle \par}\vskip 11.24pt\relax
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   592
      \noindent\ignorespaces\@subtitle \par}\vskip 17pt\relax
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   593
    \fi
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   594
    {\authorfont
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   595
    \setbox0=\vbox{\setcounter{auth}{1}\def\and{\stepcounter{auth} }%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   596
                   \hfuzz=2\textwidth\def\thanks##1{}\@author}%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   597
    \setcounter{footnote}{0}%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   598
    \global\value{inst}=\value{auth}%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   599
    \setcounter{auth}{1}%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   600
    \if@twocolumn
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   601
       \rightskip43mm plus 4cm minus 3mm
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   602
    \else % one column journal
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   603
       \rightskip=\linewidth
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   604
       \advance\rightskip by-\rubricwidth
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   605
       \advance\rightskip by0pt plus 4cm minus 3mm
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   606
    \fi
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   607
%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   608
\def\and{\unskip\nobreak\enskip{\boldmath$\cdot$}\enskip\ignorespaces}%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   609
    \noindent\ignorespaces\@author\vskip7.23pt}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   610
%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   611
    \small
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   612
    \if!\@dedic!\else
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   613
       \par
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   614
       \normalsize\it
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   615
       \addvspace\baselineskip
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   616
       \noindent\@dedic
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   617
    \fi
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   618
 \egroup % end of header box
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   619
 \@tempdima=\headerboxheight
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   620
 \advance\@tempdima by-\ht\authrun
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   621
 \unvbox\authrun
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   622
 \ifdim\@tempdima>0pt
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   623
    \vrule width0pt height\@tempdima\par
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   624
 \fi
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   625
 \noindent{\small\@date\if@twocolumn\vskip 7.2mm\else\vskip 5.2mm\fi}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   626
 \global\@minipagetrue
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   627
 \global\everypar{\global\@minipagefalse\global\everypar{}}%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   628
%\vskip22.47pt
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   629
}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   630
%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   631
\if@mathematic
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   632
   \def\vec#1{\ensuremath{\mathchoice
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   633
                     {\mbox{\boldmath$\displaystyle\mathbf{#1}$}}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   634
                     {\mbox{\boldmath$\textstyle\mathbf{#1}$}}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   635
                     {\mbox{\boldmath$\scriptstyle\mathbf{#1}$}}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   636
                     {\mbox{\boldmath$\scriptscriptstyle\mathbf{#1}$}}}}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   637
\else
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   638
   \def\vec#1{\ensuremath{\mathchoice
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   639
                     {\mbox{\boldmath$\displaystyle#1$}}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   640
                     {\mbox{\boldmath$\textstyle#1$}}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   641
                     {\mbox{\boldmath$\scriptstyle#1$}}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   642
                     {\mbox{\boldmath$\scriptscriptstyle#1$}}}}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   643
\fi
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   644
%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   645
\def\tens#1{\ensuremath{\mathsf{#1}}}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   646
%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   647
\setcounter{secnumdepth}{3}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   648
\newcounter {section}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   649
\newcounter {subsection}[section]
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   650
\newcounter {subsubsection}[subsection]
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   651
\newcounter {paragraph}[subsubsection]
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   652
\newcounter {subparagraph}[paragraph]
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   653
\renewcommand\thesection      {\@arabic\c@section}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   654
\renewcommand\thesubsection   {\thesection.\@arabic\c@subsection}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   655
\renewcommand\thesubsubsection{\thesubsection.\@arabic\c@subsubsection}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   656
\renewcommand\theparagraph    {\thesubsubsection.\@arabic\c@paragraph}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   657
\renewcommand\thesubparagraph {\theparagraph.\@arabic\c@subparagraph}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   658
%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   659
\def\@hangfrom#1{\setbox\@tempboxa\hbox{#1}%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   660
      \hangindent \z@\noindent\box\@tempboxa}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   661
%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   662
\def\@seccntformat#1{\csname the#1\endcsname\sectcounterend
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   663
\hskip\betweenumberspace}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   664
%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   665
% \newif\if@sectrule
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   666
% \if@twocolumn\else\let\@sectruletrue=\relax\fi
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   667
% \if@avier\let\@sectruletrue=\relax\fi
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   668
% \def\makesectrule{\if@sectrule\global\@sectrulefalse\null\vglue-\topskip
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   669
% \hrule\nobreak\parskip=5pt\relax\fi}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   670
% %
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   671
% \let\makesectruleori=\makesectrule
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   672
% \def\restoresectrule{\global\let\makesectrule=\makesectruleori\global\@sectrulefalse}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   673
% \def\nosectrule{\let\makesectrule=\restoresectrule}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   674
%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   675
\def\@startsection#1#2#3#4#5#6{%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   676
  \if@noskipsec \leavevmode \fi
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   677
  \par
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   678
  \@tempskipa #4\relax
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   679
  \@afterindenttrue
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   680
  \ifdim \@tempskipa <\z@
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   681
    \@tempskipa -\@tempskipa \@afterindentfalse
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   682
  \fi
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   683
  \if@nobreak
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   684
    \everypar{}%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   685
  \else
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   686
    \addpenalty\@secpenalty\addvspace\@tempskipa
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   687
  \fi
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   688
% \ifnum#2=1\relax\@sectruletrue\fi
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   689
  \@ifstar
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   690
    {\@ssect{#3}{#4}{#5}{#6}}%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   691
    {\@dblarg{\@sect{#1}{#2}{#3}{#4}{#5}{#6}}}}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   692
%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   693
\def\@sect#1#2#3#4#5#6[#7]#8{%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   694
  \ifnum #2>\c@secnumdepth
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   695
    \let\@svsec\@empty
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   696
  \else
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   697
    \refstepcounter{#1}%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   698
    \protected@edef\@svsec{\@seccntformat{#1}\relax}%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   699
  \fi
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   700
  \@tempskipa #5\relax
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   701
  \ifdim \@tempskipa>\z@
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   702
    \begingroup
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   703
      #6{% \makesectrule
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   704
        \@hangfrom{\hskip #3\relax\@svsec}%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   705
          \raggedright
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   706
          \hyphenpenalty \@M%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   707
          \interlinepenalty \@M #8\@@par}%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   708
    \endgroup
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   709
    \csname #1mark\endcsname{#7}%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   710
    \addcontentsline{toc}{#1}{%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   711
      \ifnum #2>\c@secnumdepth \else
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   712
        \protect\numberline{\csname the#1\endcsname\sectcounterend}%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   713
      \fi
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   714
      #7}%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   715
  \else
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   716
    \def\@svsechd{%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   717
      #6{\hskip #3\relax
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   718
      \@svsec #8\/\hskip\aftertext}%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   719
      \csname #1mark\endcsname{#7}%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   720
      \addcontentsline{toc}{#1}{%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   721
        \ifnum #2>\c@secnumdepth \else
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   722
          \protect\numberline{\csname the#1\endcsname}%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   723
        \fi
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   724
        #7}}%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   725
  \fi
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   726
  \@xsect{#5}}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   727
%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   728
\def\@ssect#1#2#3#4#5{%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   729
  \@tempskipa #3\relax
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   730
  \ifdim \@tempskipa>\z@
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   731
    \begingroup
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   732
      #4{% \makesectrule
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   733
        \@hangfrom{\hskip #1}%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   734
          \interlinepenalty \@M #5\@@par}%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   735
    \endgroup
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   736
  \else
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   737
    \def\@svsechd{#4{\hskip #1\relax #5}}%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   738
  \fi
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   739
  \@xsect{#3}}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   740
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   741
%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   742
% measures and setting of sections
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   743
%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   744
\def\section{\@startsection{section}{1}{\z@}%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   745
    {-21dd plus-8pt minus-4pt}{10.5dd}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   746
     {\normalsize\bfseries\boldmath}}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   747
\def\subsection{\@startsection{subsection}{2}{\z@}%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   748
    {-21dd plus-8pt minus-4pt}{10.5dd}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   749
     {\normalsize\upshape}}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   750
\def\subsubsection{\@startsection{subsubsection}{3}{\z@}%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   751
    {-13dd plus-8pt minus-4pt}{10.5dd}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   752
     {\normalsize\itshape}}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   753
\def\paragraph{\@startsection{paragraph}{4}{\z@}%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   754
    {-13pt plus-8pt minus-4pt}{\z@}{\normalsize\itshape}}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   755
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   756
\setlength\leftmargini  {\parindent}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   757
\leftmargin  \leftmargini
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   758
\setlength\leftmarginii {\parindent}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   759
\setlength\leftmarginiii {1.87em}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   760
\setlength\leftmarginiv  {1.7em}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   761
\setlength\leftmarginv  {.5em}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   762
\setlength\leftmarginvi {.5em}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   763
\setlength  \labelsep  {.5em}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   764
\setlength  \labelwidth{\leftmargini}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   765
\addtolength\labelwidth{-\labelsep}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   766
\@beginparpenalty -\@lowpenalty
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   767
\@endparpenalty   -\@lowpenalty
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   768
\@itempenalty     -\@lowpenalty
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   769
\renewcommand\theenumi{\@arabic\c@enumi}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   770
\renewcommand\theenumii{\@alph\c@enumii}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   771
\renewcommand\theenumiii{\@roman\c@enumiii}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   772
\renewcommand\theenumiv{\@Alph\c@enumiv}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   773
\newcommand\labelenumi{\theenumi.}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   774
\newcommand\labelenumii{(\theenumii)}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   775
\newcommand\labelenumiii{\theenumiii.}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   776
\newcommand\labelenumiv{\theenumiv.}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   777
\renewcommand\p@enumii{\theenumi}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   778
\renewcommand\p@enumiii{\theenumi(\theenumii)}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   779
\renewcommand\p@enumiv{\p@enumiii\theenumiii}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   780
\newcommand\labelitemi{\normalfont\bfseries --}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   781
\newcommand\labelitemii{\normalfont\bfseries --}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   782
\newcommand\labelitemiii{$\m@th\bullet$}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   783
\newcommand\labelitemiv{$\m@th\cdot$}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   784
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   785
\if@spthms
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   786
% definition of the "\spnewtheorem" command.
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   787
%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   788
% Usage:
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   789
%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   790
%     \spnewtheorem{env_nam}{caption}[within]{cap_font}{body_font}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   791
% or  \spnewtheorem{env_nam}[numbered_like]{caption}{cap_font}{body_font}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   792
% or  \spnewtheorem*{env_nam}{caption}{cap_font}{body_font}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   793
%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   794
% New is "cap_font" and "body_font". It stands for
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   795
% fontdefinition of the caption and the text itself.
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   796
%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   797
% "\spnewtheorem*" gives a theorem without number.
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   798
%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   799
% A defined spnewthoerem environment is used as described
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   800
% by Lamport.
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   801
%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   802
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   803
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   804
\def\@thmcountersep{}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   805
\def\@thmcounterend{}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   806
\newcommand\nocaption{\noexpand\@gobble}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   807
\newdimen\spthmsep \spthmsep=5pt
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   808
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   809
\def\spnewtheorem{\@ifstar{\@sthm}{\@Sthm}}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   810
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   811
% definition of \spnewtheorem with number
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   812
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   813
\def\@spnthm#1#2{%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   814
  \@ifnextchar[{\@spxnthm{#1}{#2}}{\@spynthm{#1}{#2}}}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   815
\def\@Sthm#1{\@ifnextchar[{\@spothm{#1}}{\@spnthm{#1}}}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   816
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   817
\def\@spxnthm#1#2[#3]#4#5{\expandafter\@ifdefinable\csname #1\endcsname
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   818
   {\@definecounter{#1}\@addtoreset{#1}{#3}%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   819
   \expandafter\xdef\csname the#1\endcsname{\expandafter\noexpand
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   820
     \csname the#3\endcsname \noexpand\@thmcountersep \@thmcounter{#1}}%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   821
   \expandafter\xdef\csname #1name\endcsname{#2}%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   822
   \global\@namedef{#1}{\@spthm{#1}{\csname #1name\endcsname}{#4}{#5}}%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   823
                              \global\@namedef{end#1}{\@endtheorem}}}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   824
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   825
\def\@spynthm#1#2#3#4{\expandafter\@ifdefinable\csname #1\endcsname
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   826
   {\@definecounter{#1}%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   827
   \expandafter\xdef\csname the#1\endcsname{\@thmcounter{#1}}%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   828
   \expandafter\xdef\csname #1name\endcsname{#2}%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   829
   \global\@namedef{#1}{\@spthm{#1}{\csname #1name\endcsname}{#3}{#4}}%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   830
                               \global\@namedef{end#1}{\@endtheorem}}}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   831
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   832
\def\@spothm#1[#2]#3#4#5{%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   833
  \@ifundefined{c@#2}{\@latexerr{No theorem environment `#2' defined}\@eha}%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   834
  {\expandafter\@ifdefinable\csname #1\endcsname
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   835
  {\global\@namedef{the#1}{\@nameuse{the#2}}%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   836
  \expandafter\xdef\csname #1name\endcsname{#3}%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   837
  \global\@namedef{#1}{\@spthm{#2}{\csname #1name\endcsname}{#4}{#5}}%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   838
  \global\@namedef{end#1}{\@endtheorem}}}}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   839
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   840
\def\@spthm#1#2#3#4{\topsep 7\p@ \@plus2\p@ \@minus4\p@
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   841
\labelsep=\spthmsep\refstepcounter{#1}%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   842
\@ifnextchar[{\@spythm{#1}{#2}{#3}{#4}}{\@spxthm{#1}{#2}{#3}{#4}}}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   843
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   844
\def\@spxthm#1#2#3#4{\@spbegintheorem{#2}{\csname the#1\endcsname}{#3}{#4}%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   845
                    \ignorespaces}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   846
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   847
\def\@spythm#1#2#3#4[#5]{\@spopargbegintheorem{#2}{\csname
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   848
       the#1\endcsname}{#5}{#3}{#4}\ignorespaces}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   849
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   850
\def\normalthmheadings{\def\@spbegintheorem##1##2##3##4{\trivlist\normalfont
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   851
                 \item[\hskip\labelsep{##3##1\ ##2\@thmcounterend}]##4}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   852
\def\@spopargbegintheorem##1##2##3##4##5{\trivlist
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   853
      \item[\hskip\labelsep{##4##1\ ##2}]{##4(##3)\@thmcounterend\ }##5}}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   854
\normalthmheadings
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   855
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   856
\def\reversethmheadings{\def\@spbegintheorem##1##2##3##4{\trivlist\normalfont
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   857
                 \item[\hskip\labelsep{##3##2\ ##1\@thmcounterend}]##4}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   858
\def\@spopargbegintheorem##1##2##3##4##5{\trivlist
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   859
      \item[\hskip\labelsep{##4##2\ ##1}]{##4(##3)\@thmcounterend\ }##5}}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   860
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   861
% definition of \spnewtheorem* without number
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   862
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   863
\def\@sthm#1#2{\@Ynthm{#1}{#2}}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   864
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   865
\def\@Ynthm#1#2#3#4{\expandafter\@ifdefinable\csname #1\endcsname
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   866
   {\global\@namedef{#1}{\@Thm{\csname #1name\endcsname}{#3}{#4}}%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   867
    \expandafter\xdef\csname #1name\endcsname{#2}%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   868
    \global\@namedef{end#1}{\@endtheorem}}}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   869
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   870
\def\@Thm#1#2#3{\topsep 7\p@ \@plus2\p@ \@minus4\p@
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   871
\@ifnextchar[{\@Ythm{#1}{#2}{#3}}{\@Xthm{#1}{#2}{#3}}}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   872
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   873
\def\@Xthm#1#2#3{\@Begintheorem{#1}{#2}{#3}\ignorespaces}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   874
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   875
\def\@Ythm#1#2#3[#4]{\@Opargbegintheorem{#1}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   876
       {#4}{#2}{#3}\ignorespaces}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   877
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   878
\def\@Begintheorem#1#2#3{#3\trivlist
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   879
                           \item[\hskip\labelsep{#2#1\@thmcounterend}]}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   880
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   881
\def\@Opargbegintheorem#1#2#3#4{#4\trivlist
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   882
      \item[\hskip\labelsep{#3#1}]{#3(#2)\@thmcounterend\ }}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   883
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   884
% initialize theorem environment
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   885
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   886
\if@envcntsect
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   887
   \def\@thmcountersep{.}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   888
   \spnewtheorem{theorem}{Theorem}[section]{\bfseries}{\itshape}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   889
\else
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   890
   \spnewtheorem{theorem}{Theorem}{\bfseries}{\itshape}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   891
   \if@envcntreset
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   892
      \@addtoreset{theorem}{section}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   893
   \else
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   894
      \@addtoreset{theorem}{chapter}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   895
   \fi
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   896
\fi
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   897
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   898
%definition of divers theorem environments
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   899
\spnewtheorem*{claim}{Claim}{\itshape}{\rmfamily}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   900
\spnewtheorem*{proof}{Proof}{\itshape}{\rmfamily}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   901
\if@envcntsame % all environments like "Theorem" - using its counter
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   902
   \def\spn@wtheorem#1#2#3#4{\@spothm{#1}[theorem]{#2}{#3}{#4}}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   903
\else % all environments with their own counter
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   904
   \if@envcntsect % show section counter
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   905
      \def\spn@wtheorem#1#2#3#4{\@spxnthm{#1}{#2}[section]{#3}{#4}}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   906
   \else % not numbered with section
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   907
      \if@envcntreset
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   908
         \def\spn@wtheorem#1#2#3#4{\@spynthm{#1}{#2}{#3}{#4}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   909
                                   \@addtoreset{#1}{section}}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   910
      \else
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   911
         \let\spn@wtheorem=\@spynthm
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   912
      \fi
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   913
   \fi
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   914
\fi
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   915
%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   916
\let\spdefaulttheorem=\spn@wtheorem
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   917
%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   918
\spn@wtheorem{case}{Case}{\itshape}{\rmfamily}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   919
\spn@wtheorem{conjecture}{Conjecture}{\itshape}{\rmfamily}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   920
\spn@wtheorem{corollary}{Corollary}{\bfseries}{\itshape}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   921
\spn@wtheorem{definition}{Definition}{\bfseries}{\rmfamily}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   922
\spn@wtheorem{example}{Example}{\itshape}{\rmfamily}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   923
\spn@wtheorem{exercise}{Exercise}{\bfseries}{\rmfamily}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   924
\spn@wtheorem{lemma}{Lemma}{\bfseries}{\itshape}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   925
\spn@wtheorem{note}{Note}{\itshape}{\rmfamily}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   926
\spn@wtheorem{problem}{Problem}{\bfseries}{\rmfamily}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   927
\spn@wtheorem{property}{Property}{\itshape}{\rmfamily}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   928
\spn@wtheorem{proposition}{Proposition}{\bfseries}{\itshape}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   929
\spn@wtheorem{question}{Question}{\itshape}{\rmfamily}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   930
\spn@wtheorem{solution}{Solution}{\bfseries}{\rmfamily}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   931
\spn@wtheorem{remark}{Remark}{\itshape}{\rmfamily}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   932
%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   933
\newenvironment{theopargself}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   934
    {\def\@spopargbegintheorem##1##2##3##4##5{\trivlist
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   935
         \item[\hskip\labelsep{##4##1\ ##2}]{##4##3\@thmcounterend\ }##5}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   936
     \def\@Opargbegintheorem##1##2##3##4{##4\trivlist
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   937
         \item[\hskip\labelsep{##3##1}]{##3##2\@thmcounterend\ }}}{}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   938
\newenvironment{theopargself*}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   939
    {\def\@spopargbegintheorem##1##2##3##4##5{\trivlist
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   940
         \item[\hskip\labelsep{##4##1\ ##2}]{\hspace*{-\labelsep}##4##3\@thmcounterend}##5}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   941
     \def\@Opargbegintheorem##1##2##3##4{##4\trivlist
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   942
         \item[\hskip\labelsep{##3##1}]{\hspace*{-\labelsep}##3##2\@thmcounterend}}}{}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   943
%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   944
\fi
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   945
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   946
\def\@takefromreset#1#2{%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   947
    \def\@tempa{#1}%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   948
    \let\@tempd\@elt
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   949
    \def\@elt##1{%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   950
        \def\@tempb{##1}%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   951
        \ifx\@tempa\@tempb\else
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   952
            \@addtoreset{##1}{#2}%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   953
        \fi}%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   954
    \expandafter\expandafter\let\expandafter\@tempc\csname cl@#2\endcsname
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   955
    \expandafter\def\csname cl@#2\endcsname{}%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   956
    \@tempc
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   957
    \let\@elt\@tempd}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   958
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   959
\def\squareforqed{\hbox{\rlap{$\sqcap$}$\sqcup$}}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   960
\def\qed{\ifmmode\else\unskip\quad\fi\squareforqed}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   961
\def\smartqed{\def\qed{\ifmmode\squareforqed\else{\unskip\nobreak\hfil
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   962
\penalty50\hskip1em\null\nobreak\hfil\squareforqed
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   963
\parfillskip=0pt\finalhyphendemerits=0\endgraf}\fi}}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   964
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   965
% Define `abstract' environment
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   966
\def\abstract{\topsep=0pt\partopsep=0pt\parsep=0pt\itemsep=0pt\relax
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   967
\trivlist\item[\hskip\labelsep
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   968
{\bfseries\abstractname}]\if!\abstractname!\hskip-\labelsep\fi}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   969
\if@twocolumn
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   970
% \if@avier
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   971
%   \def\endabstract{\endtrivlist\addvspace{5mm}\strich}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   972
%   \def\strich{\hrule\vskip1ptplus12pt}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   973
% \else
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   974
    \def\endabstract{\endtrivlist\addvspace{3mm}}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   975
% \fi
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   976
\else
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   977
\fi
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   978
%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   979
\newenvironment{verse}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   980
               {\let\\\@centercr
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   981
                \list{}{\itemsep      \z@
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   982
                        \itemindent   -1.5em%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   983
                        \listparindent\itemindent
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   984
                        \rightmargin  \leftmargin
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   985
                        \advance\leftmargin 1.5em}%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   986
                \item\relax}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   987
               {\endlist}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   988
\newenvironment{quotation}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   989
               {\list{}{\listparindent 1.5em%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   990
                        \itemindent    \listparindent
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   991
                        \rightmargin   \leftmargin
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   992
                        \parsep        \z@ \@plus\p@}%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   993
                \item\relax}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   994
               {\endlist}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   995
\newenvironment{quote}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   996
               {\list{}{\rightmargin\leftmargin}%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   997
                \item\relax}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   998
               {\endlist}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   999
\newcommand\appendix{\par\small
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1000
  \setcounter{section}{0}%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1001
  \setcounter{subsection}{0}%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1002
  \renewcommand\thesection{\@Alph\c@section}}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1003
\setlength\arraycolsep{1.5\p@}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1004
\setlength\tabcolsep{6\p@}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1005
\setlength\arrayrulewidth{.4\p@}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1006
\setlength\doublerulesep{2\p@}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1007
\setlength\tabbingsep{\labelsep}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1008
\skip\@mpfootins = \skip\footins
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1009
\setlength\fboxsep{3\p@}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1010
\setlength\fboxrule{.4\p@}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1011
\renewcommand\theequation{\@arabic\c@equation}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1012
\newcounter{figure}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1013
\renewcommand\thefigure{\@arabic\c@figure}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1014
\def\fps@figure{tbp}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1015
\def\ftype@figure{1}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1016
\def\ext@figure{lof}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1017
\def\fnum@figure{\figurename~\thefigure}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1018
\newenvironment{figure}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1019
               {\@float{figure}}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1020
               {\end@float}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1021
\newenvironment{figure*}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1022
               {\@dblfloat{figure}}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1023
               {\end@dblfloat}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1024
\newcounter{table}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1025
\renewcommand\thetable{\@arabic\c@table}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1026
\def\fps@table{tbp}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1027
\def\ftype@table{2}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1028
\def\ext@table{lot}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1029
\def\fnum@table{\tablename~\thetable}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1030
\newenvironment{table}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1031
               {\@float{table}}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1032
               {\end@float}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1033
\newenvironment{table*}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1034
               {\@dblfloat{table}}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1035
               {\end@dblfloat}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1036
%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1037
\def \@floatboxreset {%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1038
        \reset@font
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1039
        \small
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1040
        \@setnobreak
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1041
        \@setminipage
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1042
}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1043
%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1044
\newcommand{\tableheadseprule}{\noalign{\hrule height.375mm}}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1045
%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1046
\newlength\abovecaptionskip
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1047
\newlength\belowcaptionskip
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1048
\setlength\abovecaptionskip{10\p@}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1049
\setlength\belowcaptionskip{0\p@}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1050
\newcommand\leftlegendglue{}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1051
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1052
\def\fig@type{figure}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1053
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1054
\newdimen\figcapgap\figcapgap=3pt
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1055
\newdimen\tabcapgap\tabcapgap=5.5pt
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1056
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1057
\@ifundefined{floatlegendstyle}{\def\floatlegendstyle{\bfseries}}{}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1058
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1059
\long\def\@caption#1[#2]#3{\par\addcontentsline{\csname
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1060
  ext@#1\endcsname}{#1}{\protect\numberline{\csname
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1061
  the#1\endcsname}{\ignorespaces #2}}\begingroup
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1062
    \@parboxrestore
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1063
    \@makecaption{\csname fnum@#1\endcsname}{\ignorespaces #3}\par
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1064
  \endgroup}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1065
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1066
\def\capstrut{\vrule\@width\z@\@height\topskip}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1067
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1068
\@ifundefined{captionstyle}{\def\captionstyle{\normalfont\small}}{}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1069
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1070
\long\def\@makecaption#1#2{%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1071
 \captionstyle
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1072
 \ifx\@captype\fig@type
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1073
   \vskip\figcapgap
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1074
 \fi
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1075
 \setbox\@tempboxa\hbox{{\floatlegendstyle #1\floatcounterend}%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1076
 \capstrut #2}%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1077
 \ifdim \wd\@tempboxa >\hsize
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1078
   {\floatlegendstyle #1\floatcounterend}\capstrut #2\par
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1079
 \else
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1080
   \hbox to\hsize{\leftlegendglue\unhbox\@tempboxa\hfil}%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1081
 \fi
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1082
 \ifx\@captype\fig@type\else
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1083
   \vskip\tabcapgap
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1084
 \fi}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1085
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1086
\newdimen\figgap\figgap=1cc
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1087
\long\def\@makesidecaption#1#2{%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1088
   \parbox[b]{\@tempdimb}{\captionstyle{\floatlegendstyle
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1089
                                         #1\floatcounterend}#2}}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1090
\def\sidecaption#1\caption{%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1091
\setbox\@tempboxa=\hbox{#1\unskip}%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1092
\if@twocolumn
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1093
 \ifdim\hsize<\textwidth\else
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1094
   \ifdim\wd\@tempboxa<\columnwidth
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1095
      \typeout{Double column float fits into single column -
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1096
            ^^Jyou'd better switch the environment. }%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1097
   \fi
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1098
 \fi
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1099
\fi
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1100
\@tempdimb=\hsize
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1101
\advance\@tempdimb by-\figgap
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1102
\advance\@tempdimb by-\wd\@tempboxa
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1103
\ifdim\@tempdimb<3cm
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1104
    \typeout{\string\sidecaption: No sufficient room for the legend;
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1105
             using normal \string\caption. }%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1106
   \unhbox\@tempboxa
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1107
   \let\@capcommand=\@caption
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1108
\else
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1109
   \let\@capcommand=\@sidecaption
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1110
   \leavevmode
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1111
   \unhbox\@tempboxa
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1112
   \hfill
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1113
\fi
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1114
\refstepcounter\@captype
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1115
\@dblarg{\@capcommand\@captype}}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1116
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1117
\long\def\@sidecaption#1[#2]#3{\addcontentsline{\csname
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1118
  ext@#1\endcsname}{#1}{\protect\numberline{\csname
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1119
  the#1\endcsname}{\ignorespaces #2}}\begingroup
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1120
    \@parboxrestore
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1121
    \@makesidecaption{\csname fnum@#1\endcsname}{\ignorespaces #3}\par
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1122
  \endgroup}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1123
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1124
% Define `acknowledgement' environment
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1125
\def\acknowledgement{\par\addvspace{17pt}\small\rmfamily
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1126
\trivlist\if!\ackname!\item[]\else
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1127
\item[\hskip\labelsep
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1128
{\bfseries\ackname}]\fi}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1129
\def\endacknowledgement{\endtrivlist\addvspace{6pt}}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1130
\newenvironment{acknowledgements}{\begin{acknowledgement}}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1131
{\end{acknowledgement}}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1132
% Define `noteadd' environment
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1133
\def\noteadd{\par\addvspace{17pt}\small\rmfamily
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1134
\trivlist\item[\hskip\labelsep
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1135
{\itshape\noteaddname}]}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1136
\def\endnoteadd{\endtrivlist\addvspace{6pt}}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1137
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1138
\DeclareOldFontCommand{\rm}{\normalfont\rmfamily}{\mathrm}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1139
\DeclareOldFontCommand{\sf}{\normalfont\sffamily}{\mathsf}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1140
\DeclareOldFontCommand{\tt}{\normalfont\ttfamily}{\mathtt}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1141
\DeclareOldFontCommand{\bf}{\normalfont\bfseries}{\mathbf}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1142
\DeclareOldFontCommand{\it}{\normalfont\itshape}{\mathit}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1143
\DeclareOldFontCommand{\sl}{\normalfont\slshape}{\@nomath\sl}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1144
\DeclareOldFontCommand{\sc}{\normalfont\scshape}{\@nomath\sc}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1145
\DeclareRobustCommand*\cal{\@fontswitch\relax\mathcal}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1146
\DeclareRobustCommand*\mit{\@fontswitch\relax\mathnormal}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1147
\newcommand\@pnumwidth{1.55em}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1148
\newcommand\@tocrmarg{2.55em}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1149
\newcommand\@dotsep{4.5}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1150
\setcounter{tocdepth}{1}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1151
\newcommand\tableofcontents{%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1152
    \section*{\contentsname}%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1153
    \@starttoc{toc}%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1154
    \addtocontents{toc}{\begingroup\protect\small}%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1155
    \AtEndDocument{\addtocontents{toc}{\endgroup}}%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1156
    }
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1157
\newcommand*\l@part[2]{%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1158
  \ifnum \c@tocdepth >-2\relax
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1159
    \addpenalty\@secpenalty
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1160
    \addvspace{2.25em \@plus\p@}%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1161
    \begingroup
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1162
      \setlength\@tempdima{3em}%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1163
      \parindent \z@ \rightskip \@pnumwidth
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1164
      \parfillskip -\@pnumwidth
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1165
      {\leavevmode
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1166
       \large \bfseries #1\hfil \hb@xt@\@pnumwidth{\hss #2}}\par
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1167
       \nobreak
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1168
       \if@compatibility
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1169
         \global\@nobreaktrue
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1170
         \everypar{\global\@nobreakfalse\everypar{}}%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1171
      \fi
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1172
    \endgroup
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1173
  \fi}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1174
\newcommand*\l@section{\@dottedtocline{1}{0pt}{1.5em}}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1175
\newcommand*\l@subsection{\@dottedtocline{2}{1.5em}{2.3em}}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1176
\newcommand*\l@subsubsection{\@dottedtocline{3}{3.8em}{3.2em}}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1177
\newcommand*\l@paragraph{\@dottedtocline{4}{7.0em}{4.1em}}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1178
\newcommand*\l@subparagraph{\@dottedtocline{5}{10em}{5em}}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1179
\newcommand\listoffigures{%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1180
    \section*{\listfigurename
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1181
      \@mkboth{\listfigurename}%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1182
              {\listfigurename}}%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1183
    \@starttoc{lof}%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1184
    }
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1185
\newcommand*\l@figure{\@dottedtocline{1}{1.5em}{2.3em}}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1186
\newcommand\listoftables{%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1187
    \section*{\listtablename
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1188
      \@mkboth{\listtablename}{\listtablename}}%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1189
    \@starttoc{lot}%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1190
    }
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1191
\let\l@table\l@figure
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1192
\newdimen\bibindent
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1193
\setlength\bibindent{\parindent}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1194
\def\@biblabel#1{#1.}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1195
\def\@lbibitem[#1]#2{\item[{[#1]}\hfill]\if@filesw
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1196
      {\let\protect\noexpand
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1197
       \immediate
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1198
       \write\@auxout{\string\bibcite{#2}{#1}}}\fi\ignorespaces}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1199
\newenvironment{thebibliography}[1]
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1200
     {\section*{\refname
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1201
        \@mkboth{\refname}{\refname}}\small
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1202
      \list{\@biblabel{\@arabic\c@enumiv}}%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1203
           {\settowidth\labelwidth{\@biblabel{#1}}%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1204
            \leftmargin\labelwidth
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1205
            \advance\leftmargin\labelsep
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1206
            \@openbib@code
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1207
            \usecounter{enumiv}%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1208
            \let\p@enumiv\@empty
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1209
            \renewcommand\theenumiv{\@arabic\c@enumiv}}%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1210
      \sloppy\clubpenalty4000\widowpenalty4000%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1211
      \sfcode`\.\@m}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1212
     {\def\@noitemerr
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1213
       {\@latex@warning{Empty `thebibliography' environment}}%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1214
      \endlist}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1215
%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1216
\newcount\@tempcntc
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1217
\def\@citex[#1]#2{\if@filesw\immediate\write\@auxout{\string\citation{#2}}\fi
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1218
  \@tempcnta\z@\@tempcntb\m@ne\def\@citea{}\@cite{\@for\@citeb:=#2\do
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1219
    {\@ifundefined
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1220
       {b@\@citeb}{\@citeo\@tempcntb\m@ne\@citea\def\@citea{,}{\bfseries
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1221
        ?}\@warning
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1222
       {Citation `\@citeb' on page \thepage \space undefined}}%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1223
    {\setbox\z@\hbox{\global\@tempcntc0\csname b@\@citeb\endcsname\relax}%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1224
     \ifnum\@tempcntc=\z@ \@citeo\@tempcntb\m@ne
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1225
       \@citea\def\@citea{,\hskip0.1em\ignorespaces}\hbox{\csname b@\@citeb\endcsname}%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1226
     \else
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1227
      \advance\@tempcntb\@ne
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1228
      \ifnum\@tempcntb=\@tempcntc
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1229
      \else\advance\@tempcntb\m@ne\@citeo
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1230
      \@tempcnta\@tempcntc\@tempcntb\@tempcntc\fi\fi}}\@citeo}{#1}}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1231
\def\@citeo{\ifnum\@tempcnta>\@tempcntb\else
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1232
            \@citea\def\@citea{,\hskip0.1em\ignorespaces}%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1233
  \ifnum\@tempcnta=\@tempcntb\the\@tempcnta\else
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1234
   {\advance\@tempcnta\@ne\ifnum\@tempcnta=\@tempcntb \else \def\@citea{--}\fi
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1235
    \advance\@tempcnta\m@ne\the\@tempcnta\@citea\the\@tempcntb}\fi\fi}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1236
%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1237
\newcommand\newblock{\hskip .11em\@plus.33em\@minus.07em}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1238
\let\@openbib@code\@empty
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1239
\newenvironment{theindex}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1240
               {\if@twocolumn
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1241
                  \@restonecolfalse
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1242
                \else
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1243
                  \@restonecoltrue
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1244
                \fi
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1245
                \columnseprule \z@
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1246
                \columnsep 35\p@
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1247
                \twocolumn[\section*{\indexname}]%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1248
                \@mkboth{\indexname}{\indexname}%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1249
                \thispagestyle{plain}\parindent\z@
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1250
                \parskip\z@ \@plus .3\p@\relax
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1251
                \let\item\@idxitem}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1252
               {\if@restonecol\onecolumn\else\clearpage\fi}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1253
\newcommand\@idxitem{\par\hangindent 40\p@}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1254
\newcommand\subitem{\@idxitem \hspace*{20\p@}}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1255
\newcommand\subsubitem{\@idxitem \hspace*{30\p@}}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1256
\newcommand\indexspace{\par \vskip 10\p@ \@plus5\p@ \@minus3\p@\relax}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1257
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1258
\if@twocolumn
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1259
 \renewcommand\footnoterule{%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1260
  \kern-3\p@
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1261
  \hrule\@width\columnwidth
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1262
  \kern2.6\p@}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1263
\else
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1264
 \renewcommand\footnoterule{%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1265
  \kern-3\p@
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1266
  \hrule\@width.382\columnwidth
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1267
  \kern2.6\p@}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1268
\fi
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1269
\newcommand\@makefntext[1]{%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1270
    \noindent
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1271
    \hb@xt@\bibindent{\hss\@makefnmark\enspace}#1}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1272
%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1273
\def\trans@english{\switcht@albion}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1274
\def\trans@french{\switcht@francais}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1275
\def\trans@german{\switcht@deutsch}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1276
\newenvironment{translation}[1]{\if!#1!\else
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1277
\@ifundefined{selectlanguage}{\csname trans@#1\endcsname}{\selectlanguage{#1}}%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1278
\fi}{}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1279
% languages
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1280
% English section
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1281
\def\switcht@albion{%\typeout{English spoken.}%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1282
 \def\abstractname{Abstract}%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1283
 \def\ackname{Acknowledgements}%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1284
 \def\andname{and}%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1285
 \def\lastandname{, and}%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1286
 \def\appendixname{Appendix}%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1287
 \def\chaptername{Chapter}%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1288
 \def\claimname{Claim}%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1289
 \def\conjecturename{Conjecture}%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1290
 \def\contentsname{Contents}%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1291
 \def\corollaryname{Corollary}%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1292
 \def\definitionname{Definition}%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1293
 \def\emailname{E-mail}%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1294
 \def\examplename{Example}%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1295
 \def\exercisename{Exercise}%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1296
 \def\figurename{Fig.}%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1297
 \def\keywordname{{\bfseries Keywords}}%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1298
 \def\indexname{Index}%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1299
 \def\lemmaname{Lemma}%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1300
 \def\contriblistname{List of Contributors}%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1301
 \def\listfigurename{List of Figures}%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1302
 \def\listtablename{List of Tables}%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1303
 \def\mailname{{\itshape Correspondence to\/}:}%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1304
 \def\noteaddname{Note added in proof}%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1305
 \def\notename{Note}%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1306
 \def\partname{Part}%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1307
 \def\problemname{Problem}%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1308
 \def\proofname{Proof}%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1309
 \def\propertyname{Property}%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1310
 \def\questionname{Question}%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1311
 \def\refname{References}%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1312
 \def\remarkname{Remark}%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1313
 \def\seename{see}%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1314
 \def\solutionname{Solution}%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1315
 \def\tablename{Table}%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1316
 \def\theoremname{Theorem}%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1317
}\switcht@albion % make English default
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1318
%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1319
% French section
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1320
\def\switcht@francais{\svlanginfo
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1321
%\typeout{On parle francais.}%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1322
 \def\abstractname{R\'esum\'e\runinend}%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1323
 \def\ackname{Remerciements\runinend}%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1324
 \def\andname{et}%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1325
 \def\lastandname{ et}%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1326
 \def\appendixname{Appendice}%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1327
 \def\chaptername{Chapitre}%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1328
 \def\claimname{Pr\'etention}%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1329
 \def\conjecturename{Hypoth\`ese}%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1330
 \def\contentsname{Table des mati\`eres}%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1331
 \def\corollaryname{Corollaire}%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1332
 \def\definitionname{D\'efinition}%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1333
 \def\emailname{E-mail}%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1334
 \def\examplename{Exemple}%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1335
 \def\exercisename{Exercice}%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1336
 \def\figurename{Fig.}%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1337
 \def\keywordname{{\bfseries Mots-cl\'e\runinend}}%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1338
 \def\indexname{Index}%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1339
 \def\lemmaname{Lemme}%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1340
 \def\contriblistname{Liste des contributeurs}%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1341
 \def\listfigurename{Liste des figures}%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1342
 \def\listtablename{Liste des tables}%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1343
 \def\mailname{{\itshape Correspondence to\/}:}%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1344
 \def\noteaddname{Note ajout\'ee \`a l'\'epreuve}%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1345
 \def\notename{Remarque}%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1346
 \def\partname{Partie}%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1347
 \def\problemname{Probl\`eme}%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1348
 \def\proofname{Preuve}%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1349
 \def\propertyname{Caract\'eristique}%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1350
%\def\propositionname{Proposition}%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1351
 \def\questionname{Question}%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1352
 \def\refname{Bibliographie}%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1353
 \def\remarkname{Remarque}%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1354
 \def\seename{voyez}%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1355
 \def\solutionname{Solution}%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1356
%\def\subclassname{{\it Subject Classifications\/}:}%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1357
 \def\tablename{Tableau}%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1358
 \def\theoremname{Th\'eor\`eme}%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1359
}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1360
%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1361
% German section
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1362
\def\switcht@deutsch{\svlanginfo
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1363
%\typeout{Man spricht deutsch.}%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1364
 \def\abstractname{Zusammenfassung\runinend}%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1365
 \def\ackname{Danksagung\runinend}%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1366
 \def\andname{und}%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1367
 \def\lastandname{ und}%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1368
 \def\appendixname{Anhang}%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1369
 \def\chaptername{Kapitel}%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1370
 \def\claimname{Behauptung}%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1371
 \def\conjecturename{Hypothese}%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1372
 \def\contentsname{Inhaltsverzeichnis}%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1373
 \def\corollaryname{Korollar}%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1374
%\def\definitionname{Definition}%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1375
 \def\emailname{E-Mail}%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1376
 \def\examplename{Beispiel}%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1377
 \def\exercisename{\"Ubung}%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1378
 \def\figurename{Abb.}%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1379
 \def\keywordname{{\bfseries Schl\"usselw\"orter\runinend}}%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1380
 \def\indexname{Index}%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1381
%\def\lemmaname{Lemma}%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1382
 \def\contriblistname{Mitarbeiter}%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1383
 \def\listfigurename{Abbildungsverzeichnis}%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1384
 \def\listtablename{Tabellenverzeichnis}%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1385
 \def\mailname{{\itshape Correspondence to\/}:}%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1386
 \def\noteaddname{Nachtrag}%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1387
 \def\notename{Anmerkung}%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1388
 \def\partname{Teil}%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1389
%\def\problemname{Problem}%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1390
 \def\proofname{Beweis}%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1391
 \def\propertyname{Eigenschaft}%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1392
%\def\propositionname{Proposition}%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1393
 \def\questionname{Frage}%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1394
 \def\refname{Literatur}%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1395
 \def\remarkname{Anmerkung}%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1396
 \def\seename{siehe}%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1397
 \def\solutionname{L\"osung}%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1398
%\def\subclassname{{\it Subject Classifications\/}:}%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1399
 \def\tablename{Tabelle}%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1400
%\def\theoremname{Theorem}%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1401
}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1402
\newcommand\today{}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1403
\edef\today{\ifcase\month\or
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1404
  January\or February\or March\or April\or May\or June\or
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1405
  July\or August\or September\or October\or November\or December\fi
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1406
  \space\number\day, \number\year}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1407
\setlength\columnsep{1.5cc}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1408
\setlength\columnseprule{0\p@}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1409
%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1410
\frenchspacing
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1411
\clubpenalty=10000
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1412
\widowpenalty=10000
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1413
\def\thisbottomragged{\def\@textbottom{\vskip\z@ plus.0001fil
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1414
\global\let\@textbottom\relax}}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1415
\pagestyle{headings}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1416
\pagenumbering{arabic}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1417
\if@twocolumn
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1418
   \twocolumn
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1419
\fi
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1420
%\if@avier
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1421
%   \onecolumn
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1422
%   \setlength{\textwidth}{156mm}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1423
%   \setlength{\textheight}{226mm}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1424
%\fi
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1425
\if@referee
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1426
   \makereferee
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1427
\fi
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1428
\flushbottom
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1429
\endinput
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1430
%%
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1431
%% End of file `svjour3.cls'.