src/Doc/ProgProve/document/svmono.cls
author wenzelm
Sat, 05 Apr 2014 15:03:40 +0200
changeset 56421 1ffd7eaa778b
parent 48985 5386df44a037
permissions -rw-r--r--
updated to jedit_build-20140405: Code2HTML.jar, CommonControls.jar, Console.jar, kappalayout.jar, Navigator.jar, SideKick.jar, doc with jEdit manuals (ant dist-manuals);
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
47269
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
     1
% SVMONO DOCUMENT CLASS -- version 4.17 (31-Oct-06)
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
     2
% Springer Verlag global LaTeX2e support for monographs
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
     3
%%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
     4
%%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
     5
%% \CharacterTable
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
     6
%%  {Upper-case    \A\B\C\D\E\F\G\H\I\J\K\L\M\N\O\P\Q\R\S\T\U\V\W\X\Y\Z
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
     7
%%   Lower-case    \a\b\c\d\e\f\g\h\i\j\k\l\m\n\o\p\q\r\s\t\u\v\w\x\y\z
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
     8
%%   Digits        \0\1\2\3\4\5\6\7\8\9
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
     9
%%   Exclamation   \!     Double quote  \"     Hash (number) \#
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    10
%%   Dollar        \$     Percent       \%     Ampersand     \&
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    11
%%   Acute accent  \'     Left paren    \(     Right paren   \)
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    12
%%   Asterisk      \*     Plus          \+     Comma         \,
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    13
%%   Minus         \-     Point         \.     Solidus       \/
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    14
%%   Colon         \:     Semicolon     \;     Less than     \<
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    15
%%   Equals        \=     Greater than  \>     Question mark \?
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    16
%%   Commercial at \@     Left bracket  \[     Backslash     \\
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    17
%%   Right bracket \]     Circumflex    \^     Underscore    \_
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    18
%%   Grave accent  \`     Left brace    \{     Vertical bar  \|
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    19
%%   Right brace   \}     Tilde         \~}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    20
%%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    21
\NeedsTeXFormat{LaTeX2e}[1995/12/01]
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    22
\ProvidesClass{svmono}[2006/10/31 v4.17
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    23
^^JSpringer Verlag global LaTeX document class for monographs]
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    24
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    25
% Options
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    26
% citations
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    27
\DeclareOption{natbib}{\ExecuteOptions{oribibl}%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    28
\AtEndOfClass{% Loading package 'NATBIB'
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    29
\RequirePackage{natbib}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    30
% Changing some parameters of NATBIB
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    31
\setlength{\bibhang}{\parindent}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    32
%\setlength{\bibsep}{0mm}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    33
\let\bibfont=\small
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    34
\def\@biblabel#1{#1.}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    35
\newcommand{\etal}{\textit{et al}.}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    36
%\bibpunct[,]{(}{)}{;}{a}{}{,}}}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    37
}}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    38
% Springer environment
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    39
\let\if@spthms\iftrue
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    40
\DeclareOption{nospthms}{\let\if@spthms\iffalse}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    41
%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    42
\let\envankh\@empty   % no anchor for "theorems"
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    43
%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    44
\let\if@envcntreset\iffalse % environment counter is not reset
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    45
\let\if@envcntresetsect=\iffalse % reset each section?
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    46
\DeclareOption{envcountresetchap}{\let\if@envcntreset\iftrue}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    47
\DeclareOption{envcountresetsect}{\let\if@envcntreset\iftrue
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    48
\let\if@envcntresetsect=\iftrue}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    49
%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    50
\let\if@envcntsame\iffalse  % NOT all environments work like "Theorem",
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    51
                            % each using its own counter
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    52
\DeclareOption{envcountsame}{\let\if@envcntsame\iftrue}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    53
%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    54
\let\if@envcntshowhiercnt=\iffalse % do not show hierarchy counter at all
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    55
%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    56
% enhance theorem counter
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    57
\DeclareOption{envcountchap}{\def\envankh{chapter}% show \thechapter along with theorem number
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    58
\let\if@envcntshowhiercnt=\iftrue
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    59
\ExecuteOptions{envcountreset}}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    60
%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    61
\DeclareOption{envcountsect}{\def\envankh{section}% show \thesection along with theorem number
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    62
\let\if@envcntshowhiercnt=\iftrue
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    63
\ExecuteOptions{envcountreset}}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    64
%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    65
% languages
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    66
\let\switcht@@therlang\relax
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    67
\let\svlanginfo\relax
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    68
\def\ds@deutsch{\def\switcht@@therlang{\switcht@deutsch}%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    69
\gdef\svlanginfo{\typeout{Man spricht deutsch.}\global\let\svlanginfo\relax}}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    70
\def\ds@francais{\def\switcht@@therlang{\switcht@francais}%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    71
\gdef\svlanginfo{\typeout{On parle francais.}\global\let\svlanginfo\relax}}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    72
%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    73
\AtBeginDocument{\@ifpackageloaded{babel}{%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    74
\@ifundefined{extrasamerican}{}{\addto\extrasamerican{\switcht@albion}}%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    75
\@ifundefined{extrasaustralian}{}{\addto\extrasaustralian{\switcht@albion}}%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    76
\@ifundefined{extrasbritish}{}{\addto\extrasbritish{\switcht@albion}}%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    77
\@ifundefined{extrascanadian}{}{\addto\extrascanadian{\switcht@albion}}%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    78
\@ifundefined{extrasenglish}{}{\addto\extrasenglish{\switcht@albion}}%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    79
\@ifundefined{extrasnewzealand}{}{\addto\extrasnewzealand{\switcht@albion}}%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    80
\@ifundefined{extrasUKenglish}{}{\addto\extrasUKenglish{\switcht@albion}}%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    81
\@ifundefined{extrasUSenglish}{}{\addto\extrasUSenglish{\switcht@albion}}%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    82
\@ifundefined{captionsfrench}{}{\addto\captionsfrench{\switcht@francais}}%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    83
\@ifundefined{extrasgerman}{}{\addto\extrasgerman{\switcht@deutsch}}%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    84
\@ifundefined{extrasngerman}{}{\addto\extrasngerman{\switcht@deutsch}}%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    85
}{\switcht@@therlang}%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    86
}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    87
% numbering style of floats, equations
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    88
\newif\if@numart   \@numartfalse
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    89
\DeclareOption{numart}{\@numarttrue}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    90
\def\set@numbering{\if@numart\else\num@book\fi}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    91
\AtEndOfClass{\set@numbering}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    92
% style for vectors
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    93
\DeclareOption{vecphys}{\def\vec@style{phys}}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    94
\DeclareOption{vecarrow}{\def\vec@style{arrow}}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    95
% running heads
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    96
\let\if@runhead\iftrue
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    97
\DeclareOption{norunningheads}{\let\if@runhead\iffalse}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    98
% referee option
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    99
\let\if@referee\iffalse
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   100
\def\makereferee{\def\baselinestretch{2}\selectfont
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   101
\newbox\refereebox
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   102
\setbox\refereebox=\vbox to\z@{\vskip0.5cm%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   103
  \hbox to\textwidth{\normalsize\tt\hrulefill\lower0.5ex
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   104
        \hbox{\kern5\p@ referee's copy\kern5\p@}\hrulefill}\vss}%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   105
\def\@oddfoot{\copy\refereebox}\let\@evenfoot=\@oddfoot}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   106
\DeclareOption{referee}{\let\if@referee\iftrue
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   107
\AtBeginDocument{\makereferee\small\normalsize}}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   108
% modification of thebibliography
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   109
\let\if@openbib\iffalse
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   110
\DeclareOption{openbib}{\let\if@openbib\iftrue}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   111
% LaTeX standard, sectionwise references
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   112
\DeclareOption{oribibl}{\let\oribibl=Y}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   113
\DeclareOption{sectrefs}{\let\secbibl=Y}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   114
%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   115
% footinfo option (provides an informatory line on every page)
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   116
\def\SpringerMacroPackageNameA{svmono.cls}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   117
% \thetime, \thedate and \timstamp are macros to include
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   118
% time, date (or both) of the TeX run in the document
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   119
\def\maketimestamp{\count255=\time
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   120
\divide\count255 by 60\relax
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   121
\edef\thetime{\the\count255:}%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   122
\multiply\count255 by-60\relax
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   123
\advance\count255 by\time
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   124
\edef\thetime{\thetime\ifnum\count255<10 0\fi\the\count255}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   125
\edef\thedate{\number\day-\ifcase\month\or Jan\or Feb\or Mar\or
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   126
             Apr\or May\or Jun\or Jul\or Aug\or Sep\or Oct\or
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   127
             Nov\or Dec\fi-\number\year}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   128
\def\timstamp{\hbox to\hsize{\tt\hfil\thedate\hfil\thetime\hfil}}}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   129
\maketimestamp
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   130
%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   131
% \footinfo generates a info footline on every page containing
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   132
% pagenumber, jobname, macroname, and timestamp
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   133
\DeclareOption{footinfo}{\AtBeginDocument{\maketimestamp
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   134
   \def\ps@empty{\let\@mkboth\@gobbletwo
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   135
   \let\@oddhead\@empty\let\@evenhead\@empty}%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   136
   \def\@oddfoot{\scriptsize\tt Page:\,\thepage\space\hfil
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   137
                 job:\,\jobname\space\hfil
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   138
                 macro:\,\SpringerMacroPackageNameA\space\hfil
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   139
                 date/time:\,\thedate/\thetime}%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   140
   \let\@evenfoot=\@oddfoot}}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   141
%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   142
% start new chapter on any page
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   143
\newif\if@openright \@openrighttrue
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   144
\DeclareOption{openany}{\@openrightfalse}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   145
%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   146
% no size changing allowed
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   147
\DeclareOption{11pt}{\OptionNotUsed}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   148
\DeclareOption{12pt}{\OptionNotUsed}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   149
% options for the article class
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   150
\def\@rticle@options{10pt,twoside}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   151
% fleqn
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   152
\DeclareOption{fleqn}{\def\@rticle@options{10pt,twoside,fleqn}%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   153
\AtEndOfClass{\let\leftlegendglue\relax}%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   154
\AtBeginDocument{\mathindent\parindent}}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   155
% hanging sectioning titles
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   156
\let\if@sechang\iffalse
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   157
\DeclareOption{sechang}{\let\if@sechang\iftrue}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   158
\def\ClassInfoNoLine#1#2{%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   159
   \ClassInfo{#1}{#2\@gobble}%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   160
}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   161
\let\SVMonoOpt\@empty
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   162
\DeclareOption*{\InputIfFileExists{sv\CurrentOption.clo}{%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   163
\global\let\SVMonoOpt\CurrentOption}{%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   164
\ClassWarning{Springer-SVMono}{Specified option or subpackage
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   165
"\CurrentOption" \MessageBreak not found
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   166
passing it to article class \MessageBreak
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   167
-}\PassOptionsToClass{\CurrentOption}{article}%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   168
}}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   169
\ProcessOptions\relax
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   170
\ifx\SVMonoOpt\@empty\relax
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   171
\ClassInfoNoLine{Springer-SVMono}{extra/valid Springer sub-package
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   172
\MessageBreak not found in option list - using "global" style}{}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   173
\fi
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   174
\LoadClass[\@rticle@options]{article}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   175
\raggedbottom
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   176
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   177
% various sizes and settings for monographs
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   178
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   179
\setlength{\textwidth}{28pc}   %  11.8cm
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   180
%\setlength{\textheight}{12pt}\multiply\textheight by 45\relax
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   181
\setlength{\textheight}{540\p@}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   182
\setlength{\topmargin}{0cm}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   183
\setlength\oddsidemargin   {63\p@}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   184
\setlength\evensidemargin  {63\p@}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   185
\setlength\marginparwidth{90\p@}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   186
\setlength\headsep   {12\p@}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   187
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   188
\setlength{\parindent}{15\p@}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   189
\setlength{\parskip}{\z@ \@plus \p@}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   190
\setlength{\hfuzz}{2\p@}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   191
\setlength{\arraycolsep}{1.5\p@}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   192
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   193
\frenchspacing
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   194
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   195
\tolerance=500
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   196
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   197
\predisplaypenalty=0
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   198
\clubpenalty=10000
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   199
\widowpenalty=10000
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   200
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   201
\setlength\footnotesep{7.7\p@}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   202
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   203
\newdimen\betweenumberspace          % dimension for space between
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   204
\betweenumberspace=5\p@               % number and text of titles
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   205
\newdimen\headlineindent             % dimension for space of
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   206
\headlineindent=2.5cc                % number and gap of running heads
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   207
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   208
% fonts, sizes, and the like
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   209
\renewcommand\small{%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   210
   \@setfontsize\small\@ixpt{11}%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   211
   \abovedisplayskip 8.5\p@ \@plus3\p@ \@minus4\p@
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   212
   \abovedisplayshortskip \z@ \@plus2\p@
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   213
   \belowdisplayshortskip 4\p@ \@plus2\p@ \@minus2\p@
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   214
   \def\@listi{\leftmargin\leftmargini
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   215
               \parsep \z@ \@plus\p@ \@minus\p@
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   216
               \topsep 6\p@ \@plus2\p@ \@minus4\p@
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   217
               \itemsep\z@}%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   218
   \belowdisplayskip \abovedisplayskip
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   219
}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   220
%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   221
\let\footnotesize=\small
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   222
%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   223
\newenvironment{petit}{\par\addvspace{6\p@}\small}{\par\addvspace{6\p@}}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   224
%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   225
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   226
% modification of automatic positioning of floating objects
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   227
\setlength\@fptop{\z@ }
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   228
\setlength\@fpsep{12\p@ }
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   229
\setlength\@fpbot{\z@ \@plus 1fil }
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   230
\def\textfraction{.01}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   231
\def\floatpagefraction{.8}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   232
\setlength{\intextsep}{20\p@ \@plus 2\p@ \@minus 2\p@}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   233
\setcounter{topnumber}{4}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   234
\def\topfraction{.9}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   235
\setcounter{bottomnumber}{2}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   236
\def\bottomfraction{.7}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   237
\setcounter{totalnumber}{6}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   238
%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   239
% size and style of headings
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   240
\newcommand{\partsize}{\Large}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   241
\newcommand{\partstyle}{\bfseries\boldmath}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   242
\newcommand{\chapsize}{\Large}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   243
\newcommand{\chapstyle}{\bfseries\boldmath}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   244
\newcommand{\chapshooksize}{\small}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   245
\newcommand{\chapshookstyle}{\itshape\unboldmath}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   246
\newcommand{\secsize}{\large}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   247
\newcommand{\secstyle}{\bfseries\boldmath}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   248
\newcommand{\subsecsize}{\normalsize}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   249
\newcommand{\subsecstyle}{\bfseries\boldmath}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   250
%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   251
\def\cleardoublepage{\clearpage\if@twoside \ifodd\c@page\else
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   252
    \hbox{}\newpage\if@twocolumn\hbox{}\newpage\fi\fi\fi}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   253
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   254
\newcommand{\clearemptydoublepage}{%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   255
        \clearpage{\pagestyle{empty}\cleardoublepage}}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   256
\newcommand{\startnewpage}{\if@openright\clearemptydoublepage\else\clearpage\fi}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   257
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   258
% redefinition of \part
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   259
\renewcommand\part{\clearemptydoublepage
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   260
         \thispagestyle{empty}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   261
         \if@twocolumn
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   262
            \onecolumn
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   263
            \@tempswatrue
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   264
         \else
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   265
            \@tempswafalse
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   266
         \fi
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   267
         \@ifundefined{thispagecropped}{}{\thispagecropped}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   268
         \secdef\@part\@spart}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   269
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   270
\def\@part[#1]#2{\ifnum \c@secnumdepth >-2\relax
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   271
        \refstepcounter{part}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   272
        \addcontentsline{toc}{part}{\partname\
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   273
        \thepart\thechapterend\hspace{\betweenumberspace}%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   274
        #1}\else
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   275
        \addcontentsline{toc}{part}{#1}\fi
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   276
   \markboth{}{}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   277
   {\raggedleft
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   278
    \ifnum \c@secnumdepth >-2\relax
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   279
      \normalfont\partstyle\partsize\vrule height 34pt width 0pt depth 0pt%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   280
     \partname\ \thepart\llap{\smash{\lower 5pt\hbox to\textwidth{\hrulefill}}}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   281
    \par
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   282
    \vskip 128.3\p@ \fi
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   283
    #2\par}\@endpart}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   284
%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   285
% \@endpart finishes the part page
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   286
%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   287
\def\@endpart{\vfil\newpage
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   288
   \if@twoside
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   289
       \hbox{}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   290
       \thispagestyle{empty}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   291
       \newpage
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   292
   \fi
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   293
   \if@tempswa
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   294
     \twocolumn
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   295
   \fi}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   296
%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   297
\def\@spart#1{{\raggedleft
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   298
   \normalfont\partsize\partstyle
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   299
   #1\par}\@endpart}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   300
%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   301
\newenvironment{partbacktext}{\def\@endpart{\vfil\newpage}}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   302
{\thispagestyle{empty} \newpage \if@tempswa\twocolumn\fi}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   303
%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   304
% (re)define sectioning
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   305
\setcounter{secnumdepth}{2}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   306
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   307
\def\seccounterend{}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   308
\def\seccountergap{\hskip\betweenumberspace}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   309
\def\@seccntformat#1{\csname the#1\endcsname\seccounterend\seccountergap\ignorespaces}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   310
%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   311
\let\firstmark=\botmark
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   312
%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   313
\@ifundefined{thechapterend}{\def\thechapterend{}}{}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   314
%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   315
\if@sechang
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   316
   \def\sec@hangfrom#1{\setbox\@tempboxa\hbox{#1}%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   317
         \hangindent\wd\@tempboxa\noindent\box\@tempboxa}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   318
\else
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   319
   \def\sec@hangfrom#1{\setbox\@tempboxa\hbox{#1}%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   320
         \hangindent\z@\noindent\box\@tempboxa}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   321
\fi
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   322
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   323
\def\chap@hangfrom#1{\noindent\vrule height 34pt width 0pt depth 0pt
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   324
\rlap{\smash{\lower 5pt\hbox to\textwidth{\hrulefill}}}\hbox{#1}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   325
\vskip10pt}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   326
\def\schap@hangfrom{\chap@hangfrom{}}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   327
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   328
\newcounter{chapter}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   329
%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   330
\@addtoreset{section}{chapter}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   331
\@addtoreset{footnote}{chapter}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   332
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   333
\newif\if@mainmatter \@mainmattertrue
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   334
\newcommand\frontmatter{\startnewpage
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   335
            \@mainmatterfalse\pagenumbering{Roman}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   336
            \setcounter{page}{5}}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   337
%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   338
\newcommand\mainmatter{\clearemptydoublepage
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   339
       \@mainmattertrue\pagenumbering{arabic}}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   340
%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   341
\newcommand\backmatter{\clearemptydoublepage\@mainmatterfalse}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   342
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   343
\def\@chapapp{\chaptername}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   344
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   345
\newdimen\chapstarthookwidth
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   346
\newcommand\chapstarthook[2][0.66\textwidth]{%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   347
\setlength{\chapstarthookwidth}{#1}%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   348
\gdef\chapst@rthook{#2}}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   349
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   350
\newcommand{\processchapstarthook}{\@ifundefined{chapst@rthook}{}{%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   351
    \setbox0=\hbox{\vbox{\hyphenpenalty=50
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   352
    \begin{flushright}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   353
    \begin{minipage}{\chapstarthookwidth}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   354
       \vrule\@width\z@\@height21\p@\@depth\z@
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   355
       \normalfont\chapshooksize\chapshookstyle\chapst@rthook
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   356
    \end{minipage}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   357
    \end{flushright}}}%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   358
    \@tempdima=\pagetotal
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   359
    \advance\@tempdima by\ht0
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   360
    \ifdim\@tempdima<106\p@
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   361
       \multiply\@tempdima by-1
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   362
       \advance\@tempdima by106\p@
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   363
       \vskip\@tempdima
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   364
    \fi
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   365
    \box0\par
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   366
    \global\let\chapst@rthook=\undefined}}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   367
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   368
\newcommand\chapter{\startnewpage
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   369
                    \@ifundefined{thispagecropped}{}{\thispagecropped}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   370
                    \thispagestyle{empty}%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   371
                    \global\@topnum\z@
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   372
                    \@afterindentfalse
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   373
                    \secdef\@chapter\@schapter}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   374
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   375
\def\@chapter[#1]#2{\ifnum \c@secnumdepth >\m@ne
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   376
                       \refstepcounter{chapter}%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   377
                       \if@mainmatter
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   378
                         \typeout{\@chapapp\space\thechapter.}%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   379
                         \addcontentsline{toc}{chapter}{\protect
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   380
                                  \numberline{\thechapter\thechapterend}#1}%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   381
                       \else
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   382
                         \addcontentsline{toc}{chapter}{#1}%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   383
                       \fi
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   384
                    \else
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   385
                      \addcontentsline{toc}{chapter}{#1}%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   386
                    \fi
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   387
                    \chaptermark{#1}%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   388
                    \addtocontents{lof}{\protect\addvspace{10\p@}}%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   389
                    \addtocontents{lot}{\protect\addvspace{10\p@}}%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   390
                    \if@twocolumn
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   391
                      \@topnewpage[\@makechapterhead{#2}]%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   392
                    \else
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   393
                      \@makechapterhead{#2}%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   394
                      \@afterheading
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   395
                    \fi}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   396
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   397
\def\@schapter#1{\if@twocolumn
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   398
                   \@topnewpage[\@makeschapterhead{#1}]%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   399
                 \else
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   400
                   \@makeschapterhead{#1}%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   401
                   \@afterheading
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   402
                 \fi}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   403
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   404
%%changes position and layout of numbered chapter headings
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   405
\def\@makechapterhead#1{{\parindent\z@\raggedright\normalfont
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   406
  \hyphenpenalty \@M
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   407
  \interlinepenalty\@M
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   408
  \chapsize\chapstyle
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   409
  \chap@hangfrom{\thechapter\thechapterend\hskip\betweenumberspace}%!!!
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   410
  \ignorespaces#1\par\nobreak
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   411
  \processchapstarthook
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   412
  \ifdim\pagetotal>157\p@
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   413
     \vskip 11\p@
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   414
  \else
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   415
     \@tempdima=168\p@\advance\@tempdima by-\pagetotal
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   416
     \vskip\@tempdima
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   417
  \fi}}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   418
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   419
%%changes position and layout of unnumbered chapter headings
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   420
\def\@makeschapterhead#1{{\parindent \z@ \raggedright\normalfont
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   421
  \hyphenpenalty \@M
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   422
  \interlinepenalty\@M
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   423
  \chapsize\chapstyle
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   424
  \schap@hangfrom
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   425
  \ignorespaces#1\par\nobreak
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   426
  \processchapstarthook
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   427
  \ifdim\pagetotal>157\p@
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   428
     \vskip 11\p@
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   429
  \else
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   430
     \@tempdima=168\p@\advance\@tempdima by-\pagetotal
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   431
     \vskip\@tempdima
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   432
  \fi}}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   433
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   434
% predefined unnumbered headings
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   435
\newcommand{\preface}[1][\prefacename]{\chapter*{#1}\markboth{#1}{#1}}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   436
% same with TOC entry
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   437
\newcommand{\Preface}[1][\prefacename]{\chapter*{#1}\markboth{#1}{#1}%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   438
\addcontentsline{toc}{chapter}{#1}}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   439
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   440
% measures and setting of sections
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   441
\renewcommand\section{\@startsection{section}{1}{\z@}%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   442
                       {-24\p@ \@plus -4\p@ \@minus -4\p@}%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   443
                       {12\p@ \@plus 4\p@ \@minus 4\p@}%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   444
                       {\normalfont\secsize\secstyle
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   445
                        \rightskip=\z@ \@plus 8em\pretolerance=10000 }}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   446
\renewcommand\subsection{\@startsection{subsection}{2}{\z@}%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   447
                       {-17\p@ \@plus -4\p@ \@minus -4\p@}%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   448
                       {10\p@ \@plus 4\p@ \@minus 4\p@}%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   449
                       {\normalfont\subsecsize\subsecstyle
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   450
                        \rightskip=\z@ \@plus 8em\pretolerance=10000 }}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   451
\renewcommand\subsubsection{\@startsection{subsubsection}{3}{\z@}%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   452
                       {-17\p@ \@plus -4\p@ \@minus -4\p@}%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   453
                       {10\p@ \@plus 4\p@ \@minus 4\p@}%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   454
                       {\normalfont\normalsize\subsecstyle
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   455
                        \rightskip=\z@ \@plus 8em\pretolerance=10000 }}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   456
\renewcommand\paragraph{\@startsection{paragraph}{4}{\z@}%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   457
                       {-10\p@ \@plus -4\p@ \@minus -4\p@}%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   458
                       {10\p@ \@plus 4\p@ \@minus 4\p@}%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   459
                       {\normalfont\normalsize\itshape
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   460
                        \rightskip=\z@ \@plus 8em\pretolerance=10000 }}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   461
\def\subparagraph{\@startsection{subparagraph}{5}{\z@}%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   462
    {-5.388\p@ \@plus-4\p@ \@minus-4\p@}{-5\p@}{\normalfont\normalsize\itshape}}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   463
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   464
% Appendix
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   465
\renewcommand\appendix{\par
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   466
                \stepcounter{chapter}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   467
                \setcounter{chapter}{0}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   468
                \stepcounter{section}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   469
                \setcounter{section}{0}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   470
                \setcounter{equation}{0}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   471
                \setcounter{figure}{0}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   472
                \setcounter{table}{0}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   473
                \setcounter{footnote}{0}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   474
  \def\@chapapp{\appendixname}%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   475
  \renewcommand\thechapter{\@Alph\c@chapter}}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   476
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   477
%  definition of sections
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   478
%  \hyphenpenalty and \raggedright added, so that there is no
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   479
%  hyphenation and the text is set ragged-right in sectioning
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   480
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   481
\def\runinsep{}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   482
\def\aftertext{\unskip\runinsep}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   483
%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   484
\def\thesection{\thechapter.\arabic{section}}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   485
\def\thesubsection{\thesection.\arabic{subsection}}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   486
\def\thesubsubsection{\thesubsection.\arabic{subsubsection}}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   487
\def\theparagraph{\thesubsubsection.\arabic{paragraph}}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   488
\def\thesubparagraph{\theparagraph.\arabic{subparagraph}}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   489
\def\chaptermark#1{}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   490
%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   491
\def\@ssect#1#2#3#4#5{%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   492
  \@tempskipa #3\relax
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   493
  \ifdim \@tempskipa>\z@
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   494
    \begingroup
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   495
      #4{%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   496
        \@hangfrom{\hskip #1}%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   497
          \raggedright
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   498
          \hyphenpenalty \@M
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   499
          \interlinepenalty \@M #5\@@par}%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   500
    \endgroup
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   501
  \else
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   502
    \def\@svsechd{#4{\hskip #1\relax #5}}%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   503
  \fi
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   504
  \@xsect{#3}}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   505
%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   506
\def\@sect#1#2#3#4#5#6[#7]#8{%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   507
   \ifnum #2>\c@secnumdepth
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   508
      \let\@svsec\@empty
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   509
   \else
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   510
      \refstepcounter{#1}%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   511
      \protected@edef\@svsec{\@seccntformat{#1}\relax}%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   512
   \fi
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   513
   \@tempskipa #5\relax
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   514
   \ifdim \@tempskipa>\z@
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   515
      \begingroup #6\relax
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   516
         \sec@hangfrom{\hskip #3\relax\@svsec}%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   517
         {\raggedright
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   518
          \hyphenpenalty \@M
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   519
          \interlinepenalty \@M #8\@@par}%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   520
      \endgroup
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   521
      \csname #1mark\endcsname{#7\seccounterend}%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   522
      \addcontentsline{toc}{#1}{\ifnum #2>\c@secnumdepth
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   523
                                \else
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   524
                                   \protect\numberline{\csname the#1\endcsname\seccounterend}%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   525
                                \fi
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   526
                                #7}%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   527
   \else
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   528
      \def\@svsechd{%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   529
         #6\hskip #3\relax
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   530
         \@svsec #8\aftertext\ignorespaces
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   531
         \csname #1mark\endcsname{#7}%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   532
         \addcontentsline{toc}{#1}{%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   533
            \ifnum #2>\c@secnumdepth \else
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   534
                \protect\numberline{\csname the#1\endcsname\seccounterend}%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   535
            \fi
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   536
            #7}}%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   537
   \fi
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   538
   \@xsect{#5}}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   539
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   540
% figures and tables are processed in small print
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   541
\def \@floatboxreset {%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   542
        \reset@font
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   543
        \small
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   544
        \@setnobreak
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   545
        \@setminipage
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   546
}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   547
\def\fps@figure{htbp}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   548
\def\fps@table{htbp}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   549
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   550
% Frame for paste-in figures or tables
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   551
\def\mpicplace#1#2{%  #1 =width   #2 =height
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   552
\vbox{\hbox to #1{\vrule\@width \fboxrule \@height #2\hfill}}}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   553
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   554
% labels of enumerate
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   555
\renewcommand\labelenumii{\theenumii)}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   556
\renewcommand\theenumii{\@alph\c@enumii}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   557
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   558
% labels of itemize
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   559
\renewcommand\labelitemi{\textbullet}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   560
\renewcommand\labelitemii{\textendash}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   561
\let\labelitemiii=\labelitemiv
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   562
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   563
% labels of description
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   564
\renewcommand*\descriptionlabel[1]{\hspace\labelsep #1\hfil}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   565
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   566
% fixed indentation for standard itemize-environment
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   567
\newdimen\svitemindent \setlength{\svitemindent}{\parindent}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   568
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   569
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   570
% make indentations changeable
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   571
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   572
\def\setitemindent#1{\settowidth{\labelwidth}{#1}%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   573
        \let\setit@m=Y%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   574
        \leftmargini\labelwidth
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   575
        \advance\leftmargini\labelsep
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   576
   \def\@listi{\leftmargin\leftmargini
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   577
        \labelwidth\leftmargini\advance\labelwidth by -\labelsep
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   578
        \parsep=\parskip
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   579
        \topsep=\medskipamount
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   580
        \itemsep=\parskip \advance\itemsep by -\parsep}}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   581
\def\setitemitemindent#1{\settowidth{\labelwidth}{#1}%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   582
        \let\setit@m=Y%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   583
        \leftmarginii\labelwidth
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   584
        \advance\leftmarginii\labelsep
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   585
\def\@listii{\leftmargin\leftmarginii
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   586
        \labelwidth\leftmarginii\advance\labelwidth by -\labelsep
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   587
        \parsep=\parskip
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   588
        \topsep=\z@
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   589
        \itemsep=\parskip \advance\itemsep by -\parsep}}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   590
%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   591
% adjusted environment "description"
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   592
% if an optional parameter (at the first two levels of lists)
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   593
% is present, its width is considered to be the widest mark
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   594
% throughout the current list.
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   595
\def\description{\@ifnextchar[{\@describe}{\list{}{\labelwidth\z@
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   596
          \itemindent-\leftmargin \let\makelabel\descriptionlabel}}}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   597
%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   598
\def\describelabel#1{#1\hfil}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   599
\def\@describe[#1]{\relax\ifnum\@listdepth=0
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   600
\setitemindent{#1}\else\ifnum\@listdepth=1
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   601
\setitemitemindent{#1}\fi\fi
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   602
\list{--}{\let\makelabel\describelabel}}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   603
%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   604
\def\itemize{%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   605
  \ifnum \@itemdepth >\thr@@\@toodeep\else
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   606
    \advance\@itemdepth\@ne
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   607
    \ifx\setit@m\undefined
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   608
       \ifnum \@itemdepth=1 \leftmargini=\svitemindent
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   609
          \labelwidth\leftmargini\advance\labelwidth-\labelsep
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   610
          \leftmarginii=\leftmargini \leftmarginiii=\leftmargini
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   611
       \fi
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   612
    \fi
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   613
    \edef\@itemitem{labelitem\romannumeral\the\@itemdepth}%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   614
    \expandafter\list
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   615
      \csname\@itemitem\endcsname
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   616
      {\def\makelabel##1{\rlap{##1}\hss}}%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   617
  \fi}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   618
%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   619
\newdimen\verbatimindent \verbatimindent\parindent
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   620
\def\verbatim{\advance\@totalleftmargin by\verbatimindent
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   621
\@verbatim \frenchspacing\@vobeyspaces \@xverbatim}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   622
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   623
%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   624
%  special signs and characters
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   625
\newcommand{\D}{\mathrm{d}}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   626
\newcommand{\E}{\mathrm{e}}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   627
\let\eul=\E
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   628
\newcommand{\I}{{\rm i}}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   629
\let\imag=\I
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   630
%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   631
% the definition of uppercase Greek characters
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   632
% Springer likes them as italics to depict variables
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   633
\DeclareMathSymbol{\Gamma}{\mathalpha}{letters}{"00}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   634
\DeclareMathSymbol{\Delta}{\mathalpha}{letters}{"01}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   635
\DeclareMathSymbol{\Theta}{\mathalpha}{letters}{"02}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   636
\DeclareMathSymbol{\Lambda}{\mathalpha}{letters}{"03}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   637
\DeclareMathSymbol{\Xi}{\mathalpha}{letters}{"04}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   638
\DeclareMathSymbol{\Pi}{\mathalpha}{letters}{"05}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   639
\DeclareMathSymbol{\Sigma}{\mathalpha}{letters}{"06}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   640
\DeclareMathSymbol{\Upsilon}{\mathalpha}{letters}{"07}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   641
\DeclareMathSymbol{\Phi}{\mathalpha}{letters}{"08}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   642
\DeclareMathSymbol{\Psi}{\mathalpha}{letters}{"09}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   643
\DeclareMathSymbol{\Omega}{\mathalpha}{letters}{"0A}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   644
% the upright forms are defined here as \var<Character>
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   645
\DeclareMathSymbol{\varGamma}{\mathalpha}{operators}{"00}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   646
\DeclareMathSymbol{\varDelta}{\mathalpha}{operators}{"01}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   647
\DeclareMathSymbol{\varTheta}{\mathalpha}{operators}{"02}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   648
\DeclareMathSymbol{\varLambda}{\mathalpha}{operators}{"03}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   649
\DeclareMathSymbol{\varXi}{\mathalpha}{operators}{"04}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   650
\DeclareMathSymbol{\varPi}{\mathalpha}{operators}{"05}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   651
\DeclareMathSymbol{\varSigma}{\mathalpha}{operators}{"06}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   652
\DeclareMathSymbol{\varUpsilon}{\mathalpha}{operators}{"07}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   653
\DeclareMathSymbol{\varPhi}{\mathalpha}{operators}{"08}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   654
\DeclareMathSymbol{\varPsi}{\mathalpha}{operators}{"09}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   655
\DeclareMathSymbol{\varOmega}{\mathalpha}{operators}{"0A}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   656
% Upright Lower Case Greek letters without using a new MathAlphabet
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   657
\newcommand{\greeksym}[1]{\usefont{U}{psy}{m}{n}#1}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   658
\newcommand{\greeksymbold}[1]{{\usefont{U}{psy}{b}{n}#1}}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   659
\newcommand{\allmodesymb}[2]{\relax\ifmmode{\mathchoice
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   660
{\mbox{\fontsize{\tf@size}{\tf@size}#1{#2}}}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   661
{\mbox{\fontsize{\tf@size}{\tf@size}#1{#2}}}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   662
{\mbox{\fontsize{\sf@size}{\sf@size}#1{#2}}}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   663
{\mbox{\fontsize{\ssf@size}{\ssf@size}#1{#2}}}}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   664
\else
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   665
\mbox{#1{#2}}\fi}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   666
% Definition of lower case Greek letters
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   667
\newcommand{\ualpha}{\allmodesymb{\greeksym}{a}}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   668
\newcommand{\ubeta}{\allmodesymb{\greeksym}{b}}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   669
\newcommand{\uchi}{\allmodesymb{\greeksym}{c}}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   670
\newcommand{\udelta}{\allmodesymb{\greeksym}{d}}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   671
\newcommand{\ugamma}{\allmodesymb{\greeksym}{g}}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   672
\newcommand{\umu}{\allmodesymb{\greeksym}{m}}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   673
\newcommand{\unu}{\allmodesymb{\greeksym}{n}}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   674
\newcommand{\upi}{\allmodesymb{\greeksym}{p}}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   675
\newcommand{\utau}{\allmodesymb{\greeksym}{t}}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   676
% redefines the \vec accent to a bold character - if desired
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   677
\def\fig@type{arrow}% temporarily abused
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   678
\ifx\vec@style\fig@type\else
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   679
\@ifundefined{vec@style}{%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   680
 \def\vec#1{\ensuremath{\mathchoice
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   681
                     {\mbox{\boldmath$\displaystyle\mathbf{#1}$}}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   682
                     {\mbox{\boldmath$\textstyle\mathbf{#1}$}}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   683
                     {\mbox{\boldmath$\scriptstyle\mathbf{#1}$}}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   684
                     {\mbox{\boldmath$\scriptscriptstyle\mathbf{#1}$}}}}%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   685
}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   686
{\def\vec#1{\ensuremath{\mathchoice
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   687
                     {\mbox{\boldmath$\displaystyle#1$}}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   688
                     {\mbox{\boldmath$\textstyle#1$}}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   689
                     {\mbox{\boldmath$\scriptstyle#1$}}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   690
                     {\mbox{\boldmath$\scriptscriptstyle#1$}}}}%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   691
}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   692
\fi
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   693
% tensor
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   694
\def\tens#1{\relax\ifmmode\mathsf{#1}\else\textsf{#1}\fi}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   695
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   696
% end of proof symbol
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   697
\newcommand\qedsymbol{\hbox{\rlap{$\sqcap$}$\sqcup$}}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   698
\newcommand\qed{\relax\ifmmode\else\unskip\quad\fi\qedsymbol}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   699
\newcommand\smartqed{\renewcommand\qed{\relax\ifmmode\qedsymbol\else
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   700
  {\unskip\nobreak\hfil\penalty50\hskip1em\null\nobreak\hfil\qedsymbol
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   701
  \parfillskip=\z@\finalhyphendemerits=0\endgraf}\fi}}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   702
%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   703
\def\num@book{%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   704
\renewcommand\thesection{\thechapter.\@arabic\c@section}%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   705
\renewcommand\thesubsection{\thesection.\@arabic\c@subsection}%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   706
\renewcommand\theequation{\thechapter.\@arabic\c@equation}%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   707
\renewcommand\thefigure{\thechapter.\@arabic\c@figure}%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   708
\renewcommand\thetable{\thechapter.\@arabic\c@table}%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   709
\@addtoreset{section}{chapter}%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   710
\@addtoreset{figure}{chapter}%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   711
\@addtoreset{table}{chapter}%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   712
\@addtoreset{equation}{chapter}}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   713
%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   714
% Ragged bottom for the actual page
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   715
\def\thisbottomragged{\def\@textbottom{\vskip\z@ \@plus.0001fil
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   716
\global\let\@textbottom\relax}}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   717
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   718
% This is texte.tex
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   719
% it defines various texts and their translations
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   720
% called up with documentstyle options
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   721
\def\switcht@albion{%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   722
\def\abstractname{Summary.}%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   723
\def\ackname{Acknowledgement.}%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   724
\def\andname{and}%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   725
\def\bibname{References}%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   726
\def\lastandname{, and}%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   727
\def\appendixname{Appendix}%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   728
\def\chaptername{Chapter}%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   729
\def\claimname{Claim}%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   730
\def\conjecturename{Conjecture}%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   731
\def\contentsname{Contents}%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   732
\def\corollaryname{Corollary}%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   733
\def\definitionname{Definition}%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   734
\def\examplename{Example}%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   735
\def\exercisename{Exercise}%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   736
\def\figurename{Fig.}%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   737
\def\keywordname{{\bf Key words:}}%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   738
\def\indexname{Index}%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   739
\def\lemmaname{Lemma}%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   740
\def\contriblistname{List of Contributors}%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   741
\def\listfigurename{List of Figures}%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   742
\def\listtablename{List of Tables}%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   743
\def\mailname{{\it Correspondence to\/}:}%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   744
\def\noteaddname{Note added in proof}%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   745
\def\notename{Note}%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   746
\def\partname{Part}%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   747
\def\prefacename{Preface}%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   748
\def\problemname{Problem}%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   749
\def\proofname{Proof}%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   750
\def\propertyname{Property}%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   751
\def\propositionname{Proposition}%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   752
\def\questionname{Question}%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   753
\def\refname{References}%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   754
\def\remarkname{Remark}%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   755
\def\seename{see}%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   756
\def\solutionname{Solution}%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   757
\def\subclassname{{\it Subject Classifications\/}:}%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   758
\def\tablename{Table}%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   759
\def\theoremname{Theorem}}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   760
\switcht@albion
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   761
% Names of theorem like environments are already defined
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   762
% but must be translated if another language is chosen
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   763
%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   764
% French section
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   765
\def\switcht@francais{\svlanginfo
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   766
 \def\abstractname{R\'esum\'e.}%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   767
 \def\ackname{Remerciements.}%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   768
 \def\andname{et}%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   769
 \def\lastandname{ et}%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   770
 \def\appendixname{Appendice}%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   771
 \def\bibname{Bibliographie}%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   772
 \def\chaptername{Chapitre}%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   773
 \def\claimname{Pr\'etention}%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   774
 \def\conjecturename{Hypoth\`ese}%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   775
 \def\contentsname{Table des mati\`eres}%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   776
 \def\corollaryname{Corollaire}%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   777
 \def\definitionname{D\'efinition}%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   778
 \def\examplename{Exemple}%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   779
 \def\exercisename{Exercice}%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   780
 \def\figurename{Fig.}%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   781
 \def\keywordname{{\bf Mots-cl\'e:}}%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   782
 \def\indexname{Index}%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   783
 \def\lemmaname{Lemme}%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   784
 \def\contriblistname{Liste des contributeurs}%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   785
 \def\listfigurename{Liste des figures}%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   786
 \def\listtablename{Liste des tables}%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   787
 \def\mailname{{\it Correspondence to\/}:}%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   788
 \def\noteaddname{Note ajout\'ee \`a l'\'epreuve}%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   789
 \def\notename{Remarque}%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   790
 \def\partname{Partie}%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   791
 \def\prefacename{Avant-propos}%  ou Pr\'eface
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   792
 \def\problemname{Probl\`eme}%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   793
 \def\proofname{Preuve}%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   794
 \def\propertyname{Caract\'eristique}%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   795
%\def\propositionname{Proposition}%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   796
 \def\questionname{Question}%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   797
 \def\refname{Litt\'erature}%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   798
 \def\remarkname{Remarque}%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   799
 \def\seename{voir}%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   800
 \def\solutionname{Solution}%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   801
 \def\subclassname{{\it Subject Classifications\/}:}%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   802
 \def\tablename{Tableau}%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   803
 \def\theoremname{Th\'eor\`eme}%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   804
}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   805
%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   806
% German section
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   807
\def\switcht@deutsch{\svlanginfo
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   808
 \def\abstractname{Zusammenfassung.}%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   809
 \def\ackname{Danksagung.}%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   810
 \def\andname{und}%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   811
 \def\lastandname{ und}%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   812
 \def\appendixname{Anhang}%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   813
 \def\bibname{Literaturverzeichnis}%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   814
 \def\chaptername{Kapitel}%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   815
 \def\claimname{Behauptung}%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   816
 \def\conjecturename{Hypothese}%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   817
 \def\contentsname{Inhaltsverzeichnis}%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   818
 \def\corollaryname{Korollar}%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   819
%\def\definitionname{Definition}%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   820
 \def\examplename{Beispiel}%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   821
 \def\exercisename{\"Ubung}%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   822
 \def\figurename{Abb.}%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   823
 \def\keywordname{{\bf Schl\"usselw\"orter:}}%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   824
 \def\indexname{Sachverzeichnis}%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   825
%\def\lemmaname{Lemma}%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   826
 \def\contriblistname{Mitarbeiter}%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   827
 \def\listfigurename{Abbildungsverzeichnis}%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   828
 \def\listtablename{Tabellenverzeichnis}%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   829
 \def\mailname{{\it Correspondence to\/}:}%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   830
 \def\noteaddname{Nachtrag}%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   831
 \def\notename{Anmerkung}%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   832
 \def\partname{Teil}%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   833
 \def\prefacename{Vorwort}%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   834
%\def\problemname{Problem}%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   835
 \def\proofname{Beweis}%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   836
 \def\propertyname{Eigenschaft}%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   837
%\def\propositionname{Proposition}%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   838
 \def\questionname{Frage}%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   839
 \def\refname{Literaturverzeichnis}%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   840
 \def\remarkname{Anmerkung}%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   841
 \def\seename{siehe}%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   842
 \def\solutionname{L\"osung}%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   843
 \def\subclassname{{\it Subject Classifications\/}:}%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   844
 \def\tablename{Tabelle}%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   845
%\def\theoremname{Theorem}%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   846
}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   847
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   848
\def\getsto{\mathrel{\mathchoice {\vcenter{\offinterlineskip
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   849
\halign{\hfil
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   850
$\displaystyle##$\hfil\cr\gets\cr\to\cr}}}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   851
{\vcenter{\offinterlineskip\halign{\hfil$\textstyle##$\hfil\cr\gets
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   852
\cr\to\cr}}}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   853
{\vcenter{\offinterlineskip\halign{\hfil$\scriptstyle##$\hfil\cr\gets
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   854
\cr\to\cr}}}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   855
{\vcenter{\offinterlineskip\halign{\hfil$\scriptscriptstyle##$\hfil\cr
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   856
\gets\cr\to\cr}}}}}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   857
\def\lid{\mathrel{\mathchoice {\vcenter{\offinterlineskip\halign{\hfil
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   858
$\displaystyle##$\hfil\cr<\cr\noalign{\vskip1.2\p@}=\cr}}}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   859
{\vcenter{\offinterlineskip\halign{\hfil$\textstyle##$\hfil\cr<\cr
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   860
\noalign{\vskip1.2\p@}=\cr}}}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   861
{\vcenter{\offinterlineskip\halign{\hfil$\scriptstyle##$\hfil\cr<\cr
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   862
\noalign{\vskip\p@}=\cr}}}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   863
{\vcenter{\offinterlineskip\halign{\hfil$\scriptscriptstyle##$\hfil\cr
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   864
<\cr
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   865
\noalign{\vskip0.9\p@}=\cr}}}}}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   866
\def\gid{\mathrel{\mathchoice {\vcenter{\offinterlineskip\halign{\hfil
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   867
$\displaystyle##$\hfil\cr>\cr\noalign{\vskip1.2\p@}=\cr}}}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   868
{\vcenter{\offinterlineskip\halign{\hfil$\textstyle##$\hfil\cr>\cr
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   869
\noalign{\vskip1.2\p@}=\cr}}}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   870
{\vcenter{\offinterlineskip\halign{\hfil$\scriptstyle##$\hfil\cr>\cr
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   871
\noalign{\vskip\p@}=\cr}}}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   872
{\vcenter{\offinterlineskip\halign{\hfil$\scriptscriptstyle##$\hfil\cr
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   873
>\cr
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   874
\noalign{\vskip0.9\p@}=\cr}}}}}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   875
\def\grole{\mathrel{\mathchoice {\vcenter{\offinterlineskip
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   876
\halign{\hfil
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   877
$\displaystyle##$\hfil\cr>\cr\noalign{\vskip-\p@}<\cr}}}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   878
{\vcenter{\offinterlineskip\halign{\hfil$\textstyle##$\hfil\cr
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   879
>\cr\noalign{\vskip-\p@}<\cr}}}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   880
{\vcenter{\offinterlineskip\halign{\hfil$\scriptstyle##$\hfil\cr
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   881
>\cr\noalign{\vskip-0.8\p@}<\cr}}}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   882
{\vcenter{\offinterlineskip\halign{\hfil$\scriptscriptstyle##$\hfil\cr
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   883
>\cr\noalign{\vskip-0.3\p@}<\cr}}}}}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   884
\def\bbbr{{\rm I\!R}} %reelle Zahlen
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   885
\def\bbbm{{\rm I\!M}}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   886
\def\bbbn{{\rm I\!N}} %natuerliche Zahlen
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   887
\def\bbbf{{\rm I\!F}}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   888
\def\bbbh{{\rm I\!H}}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   889
\def\bbbk{{\rm I\!K}}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   890
\def\bbbp{{\rm I\!P}}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   891
\def\bbbone{{\mathchoice {\rm 1\mskip-4mu l} {\rm 1\mskip-4mu l}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   892
{\rm 1\mskip-4.5mu l} {\rm 1\mskip-5mu l}}}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   893
\def\bbbc{{\mathchoice {\setbox0=\hbox{$\displaystyle\rm C$}\hbox{\hbox
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   894
to\z@{\kern0.4\wd0\vrule\@height0.9\ht0\hss}\box0}}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   895
{\setbox0=\hbox{$\textstyle\rm C$}\hbox{\hbox
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   896
to\z@{\kern0.4\wd0\vrule\@height0.9\ht0\hss}\box0}}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   897
{\setbox0=\hbox{$\scriptstyle\rm C$}\hbox{\hbox
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   898
to\z@{\kern0.4\wd0\vrule\@height0.9\ht0\hss}\box0}}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   899
{\setbox0=\hbox{$\scriptscriptstyle\rm C$}\hbox{\hbox
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   900
to\z@{\kern0.4\wd0\vrule\@height0.9\ht0\hss}\box0}}}}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   901
\def\bbbq{{\mathchoice {\setbox0=\hbox{$\displaystyle\rm
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   902
Q$}\hbox{\raise
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   903
0.15\ht0\hbox to\z@{\kern0.4\wd0\vrule\@height0.8\ht0\hss}\box0}}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   904
{\setbox0=\hbox{$\textstyle\rm Q$}\hbox{\raise
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   905
0.15\ht0\hbox to\z@{\kern0.4\wd0\vrule\@height0.8\ht0\hss}\box0}}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   906
{\setbox0=\hbox{$\scriptstyle\rm Q$}\hbox{\raise
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   907
0.15\ht0\hbox to\z@{\kern0.4\wd0\vrule\@height0.7\ht0\hss}\box0}}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   908
{\setbox0=\hbox{$\scriptscriptstyle\rm Q$}\hbox{\raise
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   909
0.15\ht0\hbox to\z@{\kern0.4\wd0\vrule\@height0.7\ht0\hss}\box0}}}}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   910
\def\bbbt{{\mathchoice {\setbox0=\hbox{$\displaystyle\rm
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   911
T$}\hbox{\hbox to\z@{\kern0.3\wd0\vrule\@height0.9\ht0\hss}\box0}}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   912
{\setbox0=\hbox{$\textstyle\rm T$}\hbox{\hbox
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   913
to\z@{\kern0.3\wd0\vrule\@height0.9\ht0\hss}\box0}}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   914
{\setbox0=\hbox{$\scriptstyle\rm T$}\hbox{\hbox
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   915
to\z@{\kern0.3\wd0\vrule\@height0.9\ht0\hss}\box0}}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   916
{\setbox0=\hbox{$\scriptscriptstyle\rm T$}\hbox{\hbox
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   917
to\z@{\kern0.3\wd0\vrule\@height0.9\ht0\hss}\box0}}}}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   918
\def\bbbs{{\mathchoice
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   919
{\setbox0=\hbox{$\displaystyle     \rm S$}\hbox{\raise0.5\ht0\hbox
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   920
to\z@{\kern0.35\wd0\vrule\@height0.45\ht0\hss}\hbox
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   921
to\z@{\kern0.55\wd0\vrule\@height0.5\ht0\hss}\box0}}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   922
{\setbox0=\hbox{$\textstyle        \rm S$}\hbox{\raise0.5\ht0\hbox
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   923
to\z@{\kern0.35\wd0\vrule\@height0.45\ht0\hss}\hbox
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   924
to\z@{\kern0.55\wd0\vrule\@height0.5\ht0\hss}\box0}}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   925
{\setbox0=\hbox{$\scriptstyle      \rm S$}\hbox{\raise0.5\ht0\hbox
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   926
to\z@{\kern0.35\wd0\vrule\@height0.45\ht0\hss}\raise0.05\ht0\hbox
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   927
to\z@{\kern0.5\wd0\vrule\@height0.45\ht0\hss}\box0}}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   928
{\setbox0=\hbox{$\scriptscriptstyle\rm S$}\hbox{\raise0.5\ht0\hbox
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   929
to\z@{\kern0.4\wd0\vrule\@height0.45\ht0\hss}\raise0.05\ht0\hbox
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   930
to\z@{\kern0.55\wd0\vrule\@height0.45\ht0\hss}\box0}}}}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   931
\def\bbbz{{\mathchoice {\hbox{$\textstyle\sf Z\kern-0.4em Z$}}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   932
{\hbox{$\textstyle\sf Z\kern-0.4em Z$}}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   933
{\hbox{$\scriptstyle\sf Z\kern-0.3em Z$}}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   934
{\hbox{$\scriptscriptstyle\sf Z\kern-0.2em Z$}}}}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   935
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   936
\let\ts\,
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   937
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   938
\setlength \labelsep     {5\p@}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   939
\setlength\leftmargini   {17\p@}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   940
\setlength\leftmargin    {\leftmargini}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   941
\setlength\leftmarginii  {\leftmargini}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   942
\setlength\leftmarginiii {\leftmargini}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   943
\setlength\leftmarginiv  {\leftmargini}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   944
\setlength\labelwidth    {\leftmargini}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   945
\addtolength\labelwidth{-\labelsep}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   946
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   947
\def\@listI{\leftmargin\leftmargini
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   948
        \parsep=\parskip
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   949
        \topsep=\medskipamount
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   950
        \itemsep=\parskip \advance\itemsep by -\parsep}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   951
\let\@listi\@listI
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   952
\@listi
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   953
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   954
\def\@listii{\leftmargin\leftmarginii
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   955
        \labelwidth\leftmarginii
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   956
        \advance\labelwidth by -\labelsep
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   957
        \parsep=\parskip
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   958
        \topsep=\z@
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   959
        \itemsep=\parskip
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   960
        \advance\itemsep by -\parsep}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   961
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   962
\def\@listiii{\leftmargin\leftmarginiii
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   963
        \labelwidth\leftmarginiii\advance\labelwidth by -\labelsep
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   964
        \parsep=\parskip
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   965
        \topsep=\z@
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   966
        \itemsep=\parskip
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   967
        \advance\itemsep by -\parsep
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   968
        \partopsep=\topsep}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   969
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   970
\setlength\arraycolsep{1.5\p@}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   971
\setlength\tabcolsep{1.5\p@}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   972
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   973
\def\tableofcontents{\@restonecolfalse\if@twocolumn\@restonecoltrue\onecolumn
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   974
 \fi\chapter*{\contentsname \@mkboth{{\contentsname}}{{\contentsname}}}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   975
 \@starttoc{toc}\if@restonecol\twocolumn\fi}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   976
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   977
\setcounter{tocdepth}{2}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   978
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   979
\def\l@part#1#2{\addpenalty{\@secpenalty}%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   980
   \addvspace{2em \@plus\p@}%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   981
   \begingroup
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   982
     \parindent \z@
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   983
     \rightskip \z@ \@plus 5em
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   984
     \hrule\vskip5\p@
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   985
     \bfseries\boldmath
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   986
     \leavevmode
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   987
     #1\par
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   988
     \vskip5\p@
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   989
     \hrule
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   990
     \vskip\p@
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   991
     \nobreak
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   992
   \endgroup}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   993
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   994
\def\@dotsep{2}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   995
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   996
\def\addnumcontentsmark#1#2#3{%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   997
\addtocontents{#1}{\protect\contentsline{#2}{\protect\numberline
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   998
                                    {\thechapter}#3}{\thepage}}}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   999
\def\addcontentsmark#1#2#3{%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1000
\addtocontents{#1}{\protect\contentsline{#2}{#3}{\thepage}}}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1001
\def\addcontentsmarkwop#1#2#3{%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1002
\addtocontents{#1}{\protect\contentsline{#2}{#3}{0}}}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1003
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1004
\def\@adcmk[#1]{\ifcase #1 \or
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1005
\def\@gtempa{\addnumcontentsmark}%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1006
  \or    \def\@gtempa{\addcontentsmark}%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1007
  \or    \def\@gtempa{\addcontentsmarkwop}%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1008
  \fi\@gtempa{toc}{chapter}}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1009
\def\addtocmark{\@ifnextchar[{\@adcmk}{\@adcmk[3]}}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1010
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1011
\def\l@chapter#1#2{\par\addpenalty{-\@highpenalty}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1012
 \addvspace{1.0em \@plus \p@}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1013
 \@tempdima \tocchpnum \begingroup
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1014
 \parindent \z@ \rightskip \@tocrmarg
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1015
 \advance\rightskip by \z@ \@plus 2cm
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1016
 \parfillskip -\rightskip \pretolerance=10000
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1017
 \leavevmode \advance\leftskip\@tempdima \hskip -\leftskip
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1018
 {\bfseries\boldmath#1}\ifx0#2\hfil\null
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1019
 \else
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1020
    \nobreak
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1021
    \leaders\hbox{$\m@th \mkern \@dotsep mu\hbox{.}\mkern
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1022
    \@dotsep mu$}\hfill
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1023
    \nobreak\hbox to\@pnumwidth{\hfil #2}%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1024
 \fi\par
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1025
 \penalty\@highpenalty \endgroup}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1026
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1027
\newdimen\tocchpnum
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1028
\newdimen\tocsecnum
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1029
\newdimen\tocsectotal
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1030
\newdimen\tocsubsecnum
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1031
\newdimen\tocsubsectotal
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1032
\newdimen\tocsubsubsecnum
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1033
\newdimen\tocsubsubsectotal
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1034
\newdimen\tocparanum
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1035
\newdimen\tocparatotal
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1036
\newdimen\tocsubparanum
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1037
\tocchpnum=20\p@            % chapter {\bf 88.} \@plus 5.3\p@
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1038
\tocsecnum=22.5\p@          % section 88.8. plus 4.722\p@
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1039
\tocsubsecnum=30.5\p@       % subsection 88.8.8 plus 4.944\p@
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1040
\tocsubsubsecnum=38\p@      % subsubsection 88.8.8.8 plus 4.666\p@
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1041
\tocparanum=45\p@           % paragraph 88.8.8.8.8 plus 3.888\p@
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1042
\tocsubparanum=53\p@        % subparagraph 88.8.8.8.8.8 plus 4.11\p@
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1043
\def\calctocindent{%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1044
\tocsectotal=\tocchpnum
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1045
\advance\tocsectotal by\tocsecnum
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1046
\tocsubsectotal=\tocsectotal
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1047
\advance\tocsubsectotal by\tocsubsecnum
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1048
\tocsubsubsectotal=\tocsubsectotal
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1049
\advance\tocsubsubsectotal by\tocsubsubsecnum
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1050
\tocparatotal=\tocsubsubsectotal
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1051
\advance\tocparatotal by\tocparanum}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1052
\calctocindent
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1053
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1054
\def\@dottedtocline#1#2#3#4#5{%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1055
  \ifnum #1>\c@tocdepth \else
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1056
    \vskip \z@ \@plus.2\p@
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1057
    {\leftskip #2\relax \rightskip \@tocrmarg \advance\rightskip by \z@ \@plus 2cm
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1058
               \parfillskip -\rightskip \pretolerance=10000
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1059
     \parindent #2\relax\@afterindenttrue
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1060
     \interlinepenalty\@M
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1061
     \leavevmode
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1062
     \@tempdima #3\relax
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1063
     \advance\leftskip \@tempdima \null\nobreak\hskip -\leftskip
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1064
     {#4}\nobreak
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1065
     \leaders\hbox{$\m@th
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1066
        \mkern \@dotsep mu\hbox{.}\mkern \@dotsep
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1067
        mu$}\hfill
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1068
     \nobreak
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1069
     \hb@xt@\@pnumwidth{\hfil\normalfont \normalcolor #5}%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1070
     \par}%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1071
  \fi}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1072
%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1073
\def\l@section{\@dottedtocline{1}{\tocchpnum}{\tocsecnum}}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1074
\def\l@subsection{\@dottedtocline{2}{\tocsectotal}{\tocsubsecnum}}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1075
\def\l@subsubsection{\@dottedtocline{3}{\tocsubsectotal}{\tocsubsubsecnum}}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1076
\def\l@paragraph{\@dottedtocline{4}{\tocsubsubsectotal}{\tocparanum}}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1077
\def\l@subparagraph{\@dottedtocline{5}{\tocparatotal}{\tocsubparanum}}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1078
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1079
\renewcommand\listoffigures{%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1080
    \chapter*{\listfigurename
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1081
      \@mkboth{\listfigurename}{\listfigurename}}%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1082
    \@starttoc{lof}%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1083
    }
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1084
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1085
\renewcommand\listoftables{%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1086
    \chapter*{\listtablename
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1087
      \@mkboth{\listtablename}{\listtablename}}%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1088
    \@starttoc{lot}%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1089
    }
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1090
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1091
\renewcommand\footnoterule{%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1092
  \kern-3\p@
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1093
  \hrule\@width 50\p@
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1094
  \kern2.6\p@}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1095
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1096
\newdimen\foot@parindent
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1097
\foot@parindent 10.83\p@
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1098
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1099
\AtBeginDocument{%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1100
\long\def\@makefntext#1{\@setpar{\@@par\@tempdima \hsize
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1101
         \advance\@tempdima-\foot@parindent\parshape\@ne\foot@parindent
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1102
         \@tempdima}\par
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1103
         \parindent \foot@parindent\noindent \hbox to \z@{%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1104
         \hss\hss$^{\@thefnmark}$ }#1}}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1105
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1106
\if@spthms
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1107
% Definition of the "\spnewtheorem" command.
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1108
%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1109
% Usage:
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1110
%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1111
%     \spnewtheorem{env_nam}{caption}[within]{cap_font}{body_font}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1112
% or  \spnewtheorem{env_nam}[numbered_like]{caption}{cap_font}{body_font}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1113
% or  \spnewtheorem*{env_nam}{caption}{cap_font}{body_font}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1114
%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1115
% New is "cap_font" and "body_font". It stands for
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1116
% fontdefinition of the caption and the text itself.
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1117
%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1118
% "\spnewtheorem*" gives a theorem without number.
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1119
%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1120
% A defined spnewthoerem environment is used as described
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1121
% by Lamport.
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1122
%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1123
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1124
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1125
\def\@thmcountersep{.}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1126
\def\@thmcounterend{.}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1127
\newcommand\nocaption{\noexpand\@gobble}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1128
\newdimen\spthmsep \spthmsep=3pt
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1129
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1130
\def\spnewtheorem{\@ifstar{\@sthm}{\@Sthm}}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1131
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1132
% definition of \spnewtheorem with number
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1133
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1134
\def\@spnthm#1#2{%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1135
  \@ifnextchar[{\@spxnthm{#1}{#2}}{\@spynthm{#1}{#2}}}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1136
\def\@Sthm#1{\@ifnextchar[{\@spothm{#1}}{\@spnthm{#1}}}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1137
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1138
\def\@spxnthm#1#2[#3]#4#5{\expandafter\@ifdefinable\csname #1\endcsname
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1139
   {\@definecounter{#1}\@addtoreset{#1}{#3}%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1140
   \expandafter\xdef\csname the#1\endcsname{\expandafter\noexpand
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1141
     \csname the#3\endcsname \noexpand\@thmcountersep \@thmcounter{#1}}%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1142
   \expandafter\xdef\csname #1name\endcsname{#2}%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1143
   \global\@namedef{#1}{\@spthm{#1}{\csname #1name\endcsname}{#4}{#5}}%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1144
                              \global\@namedef{end#1}{\@endtheorem}}}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1145
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1146
\def\@spynthm#1#2#3#4{\expandafter\@ifdefinable\csname #1\endcsname
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1147
   {\@definecounter{#1}%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1148
   \expandafter\xdef\csname the#1\endcsname{\@thmcounter{#1}}%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1149
   \expandafter\xdef\csname #1name\endcsname{#2}%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1150
   \global\@namedef{#1}{\@spthm{#1}{\csname #1name\endcsname}{#3}{#4}}%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1151
                               \global\@namedef{end#1}{\@endtheorem}}}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1152
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1153
\def\@spothm#1[#2]#3#4#5{%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1154
  \@ifundefined{c@#2}{\@latexerr{No theorem environment `#2' defined}\@eha}%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1155
  {\expandafter\@ifdefinable\csname #1\endcsname
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1156
  {\global\@namedef{the#1}{\@nameuse{the#2}}%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1157
  \expandafter\xdef\csname #1name\endcsname{#3}%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1158
  \global\@namedef{#1}{\@spthm{#2}{\csname #1name\endcsname}{#4}{#5}}%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1159
  \global\@namedef{end#1}{\@endtheorem}}}}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1160
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1161
\def\@spthm#1#2#3#4{\topsep 7\p@ \@plus2\p@ \@minus4\p@
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1162
\labelsep=\spthmsep\refstepcounter{#1}%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1163
\@ifnextchar[{\@spythm{#1}{#2}{#3}{#4}}{\@spxthm{#1}{#2}{#3}{#4}}}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1164
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1165
\def\@spxthm#1#2#3#4{\@spbegintheorem{#2}{\csname the#1\endcsname}{#3}{#4}%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1166
                    \ignorespaces}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1167
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1168
\def\@spythm#1#2#3#4[#5]{\@spopargbegintheorem{#2}{\csname
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1169
       the#1\endcsname}{#5}{#3}{#4}\ignorespaces}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1170
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1171
\def\normalthmheadings{\def\@spbegintheorem##1##2##3##4{\trivlist
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1172
                 \item[\hskip\labelsep{##3##1\ ##2\@thmcounterend}]##4}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1173
\def\@spopargbegintheorem##1##2##3##4##5{\trivlist
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1174
      \item[\hskip\labelsep{##4##1\ ##2}]{##4(##3)\@thmcounterend\ }##5}}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1175
\normalthmheadings
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1176
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1177
\def\reversethmheadings{\def\@spbegintheorem##1##2##3##4{\trivlist
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1178
                 \item[\hskip\labelsep{##3##2\ ##1\@thmcounterend}]##4}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1179
\def\@spopargbegintheorem##1##2##3##4##5{\trivlist
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1180
      \item[\hskip\labelsep{##4##2\ ##1}]{##4(##3)\@thmcounterend\ }##5}}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1181
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1182
% definition of \spnewtheorem* without number
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1183
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1184
\def\@sthm#1#2{\@Ynthm{#1}{#2}}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1185
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1186
\def\@Ynthm#1#2#3#4{\expandafter\@ifdefinable\csname #1\endcsname
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1187
   {\global\@namedef{#1}{\@Thm{\csname #1name\endcsname}{#3}{#4}}%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1188
    \expandafter\xdef\csname #1name\endcsname{#2}%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1189
    \global\@namedef{end#1}{\@endtheorem}}}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1190
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1191
\def\@Thm#1#2#3{\topsep 7\p@ \@plus2\p@ \@minus4\p@
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1192
\@ifnextchar[{\@Ythm{#1}{#2}{#3}}{\@Xthm{#1}{#2}{#3}}}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1193
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1194
\def\@Xthm#1#2#3{\@Begintheorem{#1}{#2}{#3}\ignorespaces}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1195
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1196
\def\@Ythm#1#2#3[#4]{\@Opargbegintheorem{#1}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1197
       {#4}{#2}{#3}\ignorespaces}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1198
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1199
\def\@Begintheorem#1#2#3{#3\trivlist
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1200
                           \item[\hskip\labelsep{#2#1\@thmcounterend}]}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1201
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1202
\def\@Opargbegintheorem#1#2#3#4{#4\trivlist
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1203
      \item[\hskip\labelsep{#3#1}]{#3(#2)\@thmcounterend\ }}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1204
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1205
% initialize theorem environment
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1206
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1207
\if@envcntshowhiercnt % show hierarchy counter
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1208
   \def\@thmcountersep{.}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1209
   \spnewtheorem{theorem}{Theorem}[\envankh]{\bfseries}{\itshape}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1210
   \@addtoreset{theorem}{chapter}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1211
\else          % theorem counter only
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1212
   \spnewtheorem{theorem}{Theorem}{\bfseries}{\itshape}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1213
   \if@envcntreset
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1214
      \@addtoreset{theorem}{chapter}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1215
      \if@envcntresetsect
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1216
         \@addtoreset{theorem}{section}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1217
      \fi
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1218
   \fi
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1219
\fi
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1220
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1221
%definition of divers theorem environments
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1222
\spnewtheorem*{claim}{Claim}{\itshape}{\rmfamily}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1223
\spnewtheorem*{proof}{Proof}{\itshape}{\rmfamily}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1224
%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1225
\if@envcntsame % all environments like "Theorem" - using its counter
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1226
   \def\spn@wtheorem#1#2#3#4{\@spothm{#1}[theorem]{#2}{#3}{#4}}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1227
\else % all environments with their own counter
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1228
   \if@envcntshowhiercnt % show hierarchy counter
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1229
      \def\spn@wtheorem#1#2#3#4{\@spxnthm{#1}{#2}[\envankh]{#3}{#4}}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1230
   \else          % environment counter only
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1231
      \if@envcntreset % environment counter is reset each section
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1232
         \if@envcntresetsect
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1233
            \def\spn@wtheorem#1#2#3#4{\@spynthm{#1}{#2}{#3}{#4}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1234
             \@addtoreset{#1}{chapter}\@addtoreset{#1}{section}}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1235
         \else
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1236
            \def\spn@wtheorem#1#2#3#4{\@spynthm{#1}{#2}{#3}{#4}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1237
                                      \@addtoreset{#1}{chapter}}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1238
         \fi
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1239
      \else
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1240
         \let\spn@wtheorem=\@spynthm
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1241
      \fi
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1242
   \fi
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1243
\fi
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1244
%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1245
\let\spdefaulttheorem=\spn@wtheorem
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1246
%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1247
\spn@wtheorem{case}{Case}{\itshape}{\rmfamily}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1248
\spn@wtheorem{conjecture}{Conjecture}{\itshape}{\rmfamily}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1249
\spn@wtheorem{corollary}{Corollary}{\bfseries}{\itshape}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1250
\spn@wtheorem{definition}{Definition}{\bfseries}{\itshape}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1251
\spn@wtheorem{example}{Example}{\itshape}{\rmfamily}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1252
\spn@wtheorem{exercise}{Exercise}{\bfseries}{\rmfamily}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1253
\spn@wtheorem{lemma}{Lemma}{\bfseries}{\itshape}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1254
\spn@wtheorem{note}{Note}{\itshape}{\rmfamily}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1255
\spn@wtheorem{problem}{Problem}{\bfseries}{\rmfamily}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1256
\spn@wtheorem{property}{Property}{\itshape}{\rmfamily}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1257
\spn@wtheorem{proposition}{Proposition}{\bfseries}{\itshape}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1258
\spn@wtheorem{question}{Question}{\itshape}{\rmfamily}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1259
\spn@wtheorem{solution}{Solution}{\bfseries}{\rmfamily}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1260
\spn@wtheorem{remark}{Remark}{\itshape}{\rmfamily}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1261
%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1262
\newenvironment{theopargself}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1263
    {\def\@spopargbegintheorem##1##2##3##4##5{\trivlist
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1264
         \item[\hskip\labelsep{##4##1\ ##2}]{##4##3\@thmcounterend\ }##5}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1265
     \def\@Opargbegintheorem##1##2##3##4{##4\trivlist
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1266
         \item[\hskip\labelsep{##3##1}]{##3##2\@thmcounterend\ }}}{}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1267
\newenvironment{theopargself*}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1268
    {\def\@spopargbegintheorem##1##2##3##4##5{\trivlist
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1269
         \item[\hskip\labelsep{##4##1\ ##2}]{\hspace*{-\labelsep}##4##3\@thmcounterend}##5}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1270
     \def\@Opargbegintheorem##1##2##3##4{##4\trivlist
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1271
         \item[\hskip\labelsep{##3##1}]{\hspace*{-\labelsep}##3##2\@thmcounterend}}}{}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1272
%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1273
\spnewtheorem{prob}{\nocaption}[chapter]{\bfseries}{\rmfamily}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1274
\newcommand{\probref}[1]{\textbf{\ref{#1}} }
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1275
\newenvironment{sol}{\par\addvspace{6pt}\noindent\probref}{\par\addvspace{6pt}}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1276
%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1277
\fi
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1278
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1279
\def\@takefromreset#1#2{%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1280
    \def\@tempa{#1}%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1281
    \let\@tempd\@elt
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1282
    \def\@elt##1{%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1283
        \def\@tempb{##1}%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1284
        \ifx\@tempa\@tempb\else
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1285
            \@addtoreset{##1}{#2}%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1286
        \fi}%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1287
    \expandafter\expandafter\let\expandafter\@tempc\csname cl@#2\endcsname
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1288
    \expandafter\def\csname cl@#2\endcsname{}%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1289
    \@tempc
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1290
    \let\@elt\@tempd}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1291
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1292
% redefininition of the captions for "figure" and "table" environments
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1293
%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1294
\@ifundefined{floatlegendstyle}{\def\floatlegendstyle{\bfseries}}{}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1295
\def\floatcounterend{.\ }
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1296
\def\capstrut{\vrule\@width\z@\@height\topskip}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1297
\@ifundefined{captionstyle}{\def\captionstyle{\normalfont\small}}{}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1298
\@ifundefined{instindent}{\newdimen\instindent}{}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1299
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1300
\long\def\@caption#1[#2]#3{\par\addcontentsline{\csname
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1301
  ext@#1\endcsname}{#1}{\protect\numberline{\csname
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1302
  the#1\endcsname}{\ignorespaces #2}}\begingroup
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1303
    \@parboxrestore\if@minipage\@setminipage\fi
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1304
    \@makecaption{\csname fnum@#1\endcsname}{\ignorespaces #3}\par
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1305
  \endgroup}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1306
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1307
\def\twocaptionwidth#1#2{\def\first@capwidth{#1}\def\second@capwidth{#2}}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1308
% Default: .46\textwidth
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1309
\twocaptionwidth{.46\textwidth}{.46\textwidth}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1310
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1311
\def\leftcaption{\refstepcounter\@captype\@dblarg%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1312
            {\@leftcaption\@captype}}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1313
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1314
\def\rightcaption{\refstepcounter\@captype\@dblarg%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1315
            {\@rightcaption\@captype}}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1316
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1317
\long\def\@leftcaption#1[#2]#3{\addcontentsline{\csname
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1318
  ext@#1\endcsname}{#1}{\protect\numberline{\csname
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1319
  the#1\endcsname}{\ignorespaces #2}}\begingroup
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1320
    \@parboxrestore
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1321
    \vskip\figcapgap
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1322
    \@maketwocaptions{\csname fnum@#1\endcsname}{\ignorespaces #3}%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1323
    {\first@capwidth}\ignorespaces\hspace{.073\textwidth}\hfill%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1324
  \endgroup}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1325
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1326
\long\def\@rightcaption#1[#2]#3{\addcontentsline{\csname
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1327
  ext@#1\endcsname}{#1}{\protect\numberline{\csname
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1328
  the#1\endcsname}{\ignorespaces #2}}\begingroup
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1329
    \@parboxrestore
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1330
    \@maketwocaptions{\csname fnum@#1\endcsname}{\ignorespaces #3}%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1331
    {\second@capwidth}\par
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1332
  \endgroup}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1333
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1334
\long\def\@maketwocaptions#1#2#3{%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1335
   \parbox[t]{#3}{{\floatlegendstyle #1\floatcounterend}#2}}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1336
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1337
\def\fig@pos{l}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1338
\newcommand{\leftfigure}[2][\fig@pos]{\makebox[.4635\textwidth][#1]{#2}}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1339
\let\rightfigure\leftfigure
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1340
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1341
\newdimen\figgap\figgap=0.5cm  % hgap between figure and sidecaption
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1342
%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1343
\long\def\@makesidecaption#1#2{%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1344
   \setbox0=\vbox{\hsize=\@tempdimb
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1345
                  \captionstyle{\floatlegendstyle
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1346
                                         #1\floatcounterend}#2}%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1347
   \ifdim\instindent<\z@
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1348
      \ifdim\ht0>-\instindent
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1349
         \advance\instindent by\ht0
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1350
         \typeout{^^JClass-Warning: Legend of \string\sidecaption\space for
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1351
                     \@captype\space\csname the\@captype\endcsname
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1352
                  ^^Jis \the\instindent\space taller than the corresponding float -
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1353
                  ^^Jyou'd better switch the environment. }%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1354
         \instindent\z@
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1355
      \fi
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1356
   \else
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1357
      \ifdim\ht0<\instindent
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1358
         \advance\instindent by-\ht0
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1359
         \advance\instindent by-\dp0\relax
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1360
         \advance\instindent by\topskip
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1361
         \advance\instindent by-11\p@
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1362
      \else
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1363
         \advance\instindent by-\ht0
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1364
         \instindent=-\instindent
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1365
         \typeout{^^JClass-Warning: Legend of \string\sidecaption\space for
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1366
                     \@captype\space\csname the\@captype\endcsname
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1367
                  ^^Jis \the\instindent\space taller than the corresponding float -
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1368
                  ^^Jyou'd better switch the environment. }%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1369
         \instindent\z@
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1370
      \fi
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1371
   \fi
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1372
   \parbox[b]{\@tempdimb}{\captionstyle{\floatlegendstyle
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1373
                                        #1\floatcounterend}#2%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1374
                          \ifdim\instindent>\z@ \\
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1375
                               \vrule\@width\z@\@height\instindent
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1376
                                     \@depth\z@
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1377
                          \fi}}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1378
\def\sidecaption{\@ifnextchar[\sidec@ption{\sidec@ption[b]}}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1379
\def\sidec@ption[#1]#2\caption{%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1380
\setbox\@tempboxa=\hbox{\ignorespaces#2\unskip}%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1381
\if@twocolumn
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1382
 \ifdim\hsize<\textwidth\else
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1383
   \ifdim\wd\@tempboxa<\columnwidth
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1384
      \typeout{Double column float fits into single column -
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1385
            ^^Jyou'd better switch the environment. }%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1386
   \fi
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1387
 \fi
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1388
\fi
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1389
  \instindent=\ht\@tempboxa
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1390
  \advance\instindent by\dp\@tempboxa
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1391
\if t#1
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1392
\else
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1393
  \instindent=-\instindent
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1394
\fi
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1395
\@tempdimb=\hsize
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1396
\advance\@tempdimb by-\figgap
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1397
\advance\@tempdimb by-\wd\@tempboxa
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1398
\ifdim\@tempdimb<3cm
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1399
   \ClassWarning{SVMono}{\string\sidecaption: No sufficient room for the legend;
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1400
             ^^Jusing normal \string\caption}%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1401
   \unhbox\@tempboxa
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1402
   \let\@capcommand=\@caption
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1403
\else
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1404
   \ifdim\@tempdimb<4.5cm
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1405
      \ClassWarning{SVMono}{\string\sidecaption: Room for the legend very narrow;
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1406
               ^^Jusing \string\raggedright}%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1407
      \toks@\expandafter{\captionstyle\sloppy
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1408
                         \rightskip=\z@\@plus6mm\relax}%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1409
      \def\captionstyle{\the\toks@}%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1410
   \fi
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1411
   \let\@capcommand=\@sidecaption
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1412
   \leavevmode
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1413
   \unhbox\@tempboxa
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1414
   \hfill
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1415
\fi
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1416
\refstepcounter\@captype
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1417
\@dblarg{\@capcommand\@captype}}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1418
\long\def\@sidecaption#1[#2]#3{\addcontentsline{\csname
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1419
  ext@#1\endcsname}{#1}{\protect\numberline{\csname
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1420
  the#1\endcsname}{\ignorespaces #2}}\begingroup
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1421
    \@parboxrestore
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1422
    \@makesidecaption{\csname fnum@#1\endcsname}{\ignorespaces #3}\par
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1423
  \endgroup}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1424
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1425
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1426
\def\fig@type{figure}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1427
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1428
\def\leftlegendglue{\hfil}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1429
\newdimen\figcapgap\figcapgap=5\p@   % vgap between figure and caption
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1430
\newdimen\tabcapgap\tabcapgap=5.5\p@ % vgap between caption and table
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1431
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1432
\long\def\@makecaption#1#2{%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1433
 \captionstyle
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1434
 \ifx\@captype\fig@type
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1435
   \vskip\figcapgap
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1436
 \fi
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1437
 \setbox\@tempboxa\hbox{{\floatlegendstyle #1\floatcounterend}%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1438
 \capstrut #2}%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1439
 \ifdim \wd\@tempboxa >\hsize
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1440
   {\floatlegendstyle #1\floatcounterend}\capstrut #2\par
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1441
 \else
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1442
   \hbox to\hsize{\leftlegendglue\unhbox\@tempboxa\hfil}%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1443
 \fi
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1444
 \ifx\@captype\fig@type\else
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1445
   \vskip\tabcapgap
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1446
 \fi}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1447
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1448
\newcounter{merk}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1449
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1450
\def\endfigure{\resetsubfig\end@float}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1451
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1452
\@namedef{endfigure*}{\resetsubfig\end@dblfloat}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1453
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1454
\def\resetsubfig{\global\let\last@subfig=\undefined}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1455
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1456
\def\r@setsubfig{\xdef\last@subfig{\number\value{figure}}%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1457
\setcounter{figure}{\value{merk}}%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1458
\setcounter{merk}{0}}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1459
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1460
\def\subfigures{\refstepcounter{figure}%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1461
   \@tempcnta=\value{merk}%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1462
   \setcounter{merk}{\value{figure}}%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1463
   \setcounter{figure}{\the\@tempcnta}%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1464
   \def\thefigure{\if@numart\else\thechapter.\fi
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1465
   \@arabic\c@merk\alph{figure}}%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1466
   \let\resetsubfig=\r@setsubfig}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1467
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1468
\def\samenumber{\addtocounter{\@captype}{-1}%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1469
\@ifundefined{last@subfig}{}{\setcounter{merk}{\last@subfig}}}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1470
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1471
% redefinition of the "bibliography" environment
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1472
%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1473
\def\biblstarthook#1{\gdef\biblst@rthook{#1}}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1474
%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1475
\AtBeginDocument{%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1476
\ifx\secbibl\undefined
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1477
   \def\bibsection{\chapter*{\refname}\markboth{\refname}{\refname}%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1478
      \addcontentsline{toc}{chapter}{\refname}%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1479
      \csname biblst@rthook\endcsname}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1480
\else
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1481
   \def\bibsection{\section*{\refname}\markright{\refname}%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
  1482
      \addcontentsline{toc}{sect