doc-src/iman.sty
author wenzelm
Fri, 30 Jul 1999 15:57:50 +0200
changeset 7139 1af4c1f48368
parent 7043 96d4aa129be1
child 7169 76ef91b608a9
permissions -rw-r--r--
added \text;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
293
63a0077dd9f2 first draft of Springer volume
lcp
parents: 140
diff changeset
     1
% iman.sty : Isabelle Manual Page Layout
110
a931f1b45151 new style file
lcp
parents:
diff changeset
     2
%
293
63a0077dd9f2 first draft of Springer volume
lcp
parents: 140
diff changeset
     3
\typeout{Document Style iman. Released 17 February 1994}
110
a931f1b45151 new style file
lcp
parents:
diff changeset
     4
293
63a0077dd9f2 first draft of Springer volume
lcp
parents: 140
diff changeset
     5
\hyphenation{Isa-belle man-u-script man-u-scripts ap-pen-dix mut-u-al-ly}
63a0077dd9f2 first draft of Springer volume
lcp
parents: 140
diff changeset
     6
\hyphenation{data-type data-types co-data-type co-data-types }
63a0077dd9f2 first draft of Springer volume
lcp
parents: 140
diff changeset
     7
63a0077dd9f2 first draft of Springer volume
lcp
parents: 140
diff changeset
     8
\let\ts=\thinspace
110
a931f1b45151 new style file
lcp
parents:
diff changeset
     9
301
f5ccfc4d362f added \iflabelundefined
lcp
parents: 293
diff changeset
    10
%usage: \iflabelundefined{LABEL}{if not defined}{if defined}
f5ccfc4d362f added \iflabelundefined
lcp
parents: 293
diff changeset
    11
\newcommand{\iflabelundefined}[1]{\@ifundefined{r@#1}}
f5ccfc4d362f added \iflabelundefined
lcp
parents: 293
diff changeset
    12
f5ccfc4d362f added \iflabelundefined
lcp
parents: 293
diff changeset
    13
110
a931f1b45151 new style file
lcp
parents:
diff changeset
    14
%%%INDEXING  use sedindex to process the index
a931f1b45151 new style file
lcp
parents:
diff changeset
    15
%index, putting page numbers of definitions in boldface
6747
cee5adcc1f5c \def\bold;
wenzelm
parents: 6123
diff changeset
    16
\def\bold#1{\textbf{#1}}
293
63a0077dd9f2 first draft of Springer volume
lcp
parents: 140
diff changeset
    17
\newcommand\fnote[1]{#1n}
110
a931f1b45151 new style file
lcp
parents:
diff changeset
    18
\newcommand\indexbold[1]{\index{#1|bold}}
a931f1b45151 new style file
lcp
parents:
diff changeset
    19
350
d9ebca601847 post-CRC corrections
lcp
parents: 301
diff changeset
    20
%for indexing constants, symbols, theorems, ...
d9ebca601847 post-CRC corrections
lcp
parents: 301
diff changeset
    21
\newcommand\cdx[1]{{\tt#1}\index{#1@{\tt#1} constant}}
d9ebca601847 post-CRC corrections
lcp
parents: 301
diff changeset
    22
\newcommand\sdx[1]{{\tt#1}\index{#1@{\tt#1} symbol}}
d9ebca601847 post-CRC corrections
lcp
parents: 301
diff changeset
    23
d9ebca601847 post-CRC corrections
lcp
parents: 301
diff changeset
    24
\newcommand\tdx[1]{{\tt#1}\index{#1@{\tt#1} theorem}}
d9ebca601847 post-CRC corrections
lcp
parents: 301
diff changeset
    25
\newcommand\tdxbold[1]{{\tt#1}\index{#1@{\tt#1} theorem|bold}}
d9ebca601847 post-CRC corrections
lcp
parents: 301
diff changeset
    26
d9ebca601847 post-CRC corrections
lcp
parents: 301
diff changeset
    27
\newcommand\mltydx[1]{{\tt#1}\index{#1@{\tt#1} ML type}}
d9ebca601847 post-CRC corrections
lcp
parents: 301
diff changeset
    28
\newcommand\xdx[1]{{\tt#1}\index{#1@{\tt#1} exception}}
d9ebca601847 post-CRC corrections
lcp
parents: 301
diff changeset
    29
d9ebca601847 post-CRC corrections
lcp
parents: 301
diff changeset
    30
\newcommand\ndx[1]{{\tt#1}\index{#1@{\tt#1} nonterminal}}
d9ebca601847 post-CRC corrections
lcp
parents: 301
diff changeset
    31
\newcommand\ndxbold[1]{{\tt#1}\index{#1@{\tt#1} nonterminal|bold}}
d9ebca601847 post-CRC corrections
lcp
parents: 301
diff changeset
    32
d9ebca601847 post-CRC corrections
lcp
parents: 301
diff changeset
    33
\newcommand\cldx[1]{{\tt#1}\index{#1@{\tt#1} class}}
3491
59ffc1c83403 Modified the \tydx command to set types in italics instead of \tt
paulson
parents: 3211
diff changeset
    34
\newcommand\tydx[1]{\textit{#1}\index{#1@{\textit{#1}} type}}
350
d9ebca601847 post-CRC corrections
lcp
parents: 301
diff changeset
    35
\newcommand\thydx[1]{{\tt#1}\index{#1@{\tt#1} theory}}
d9ebca601847 post-CRC corrections
lcp
parents: 301
diff changeset
    36
3187
8f8c88dcd728 added \tooldx;
wenzelm
parents: 3109
diff changeset
    37
\newcommand\tooldx[1]{{\tt#1}\index{#1@{\tt#1} tool}}
3211
57a9b613036e added \settdx;
wenzelm
parents: 3187
diff changeset
    38
\newcommand\settdx[1]{{\tt#1}\index{#1@{\tt#1} setting}}
7043
96d4aa129be1 added attdx, methdx;
wenzelm
parents: 6747
diff changeset
    39
\newcommand\attdx[1]{{\tt#1}\index{#1@{\tt#1} attribute}}
96d4aa129be1 added attdx, methdx;
wenzelm
parents: 6747
diff changeset
    40
\newcommand\methdx[1]{{\tt#1}\index{#1@{\tt#1} proof method}}
3187
8f8c88dcd728 added \tooldx;
wenzelm
parents: 3109
diff changeset
    41
110
a931f1b45151 new style file
lcp
parents:
diff changeset
    42
%for cross-references: 2nd argument (page number) is ignored
a931f1b45151 new style file
lcp
parents:
diff changeset
    43
\newcommand\see[2]{{\it see \/}{#1}}
a931f1b45151 new style file
lcp
parents:
diff changeset
    44
\newcommand\seealso[2]{{\it see also \/}{#1}}
a931f1b45151 new style file
lcp
parents:
diff changeset
    45
3100
2b0f9ff06018 fixed comment;
wenzelm
parents: 3096
diff changeset
    46
%set argument in \tt font; at the same time, index using * prefix
350
d9ebca601847 post-CRC corrections
lcp
parents: 301
diff changeset
    47
\newcommand\rmindex[1]{{#1}\index{#1}\@}
110
a931f1b45151 new style file
lcp
parents:
diff changeset
    48
\newcommand\ttindex[1]{{\tt#1}\index{*#1}\@}
a931f1b45151 new style file
lcp
parents:
diff changeset
    49
\newcommand\ttindexbold[1]{{\tt#1}\index{*#1|bold}\@}
a931f1b45151 new style file
lcp
parents:
diff changeset
    50
a931f1b45151 new style file
lcp
parents:
diff changeset
    51
%set argument in \bf font and index in ROMAN font (for definitions in text!)
a931f1b45151 new style file
lcp
parents:
diff changeset
    52
\newcommand\bfindex[1]{{\bf#1}\index{#1|bold}\@}
a931f1b45151 new style file
lcp
parents:
diff changeset
    53
a931f1b45151 new style file
lcp
parents:
diff changeset
    54
a931f1b45151 new style file
lcp
parents:
diff changeset
    55
%%% underscores as ordinary characters, not for subscripting
a931f1b45151 new style file
lcp
parents:
diff changeset
    56
%%  use @ or \sb for subscripting; use \at for @
a931f1b45151 new style file
lcp
parents:
diff changeset
    57
%%  only works in \tt font
a931f1b45151 new style file
lcp
parents:
diff changeset
    58
%%  must not make _ an active char; would make \ttindex fail!
a931f1b45151 new style file
lcp
parents:
diff changeset
    59
\gdef\underscoreoff{\catcode`\@=8\catcode`\_=\other}
a931f1b45151 new style file
lcp
parents:
diff changeset
    60
\gdef\underscoreon{\catcode`\_=8\makeatother}
a931f1b45151 new style file
lcp
parents:
diff changeset
    61
\chardef\other=12
a931f1b45151 new style file
lcp
parents:
diff changeset
    62
\chardef\at=`\@
a931f1b45151 new style file
lcp
parents:
diff changeset
    63
a931f1b45151 new style file
lcp
parents:
diff changeset
    64
% alternative underscore
a931f1b45151 new style file
lcp
parents:
diff changeset
    65
\def\_{\leavevmode\kern.06em\vbox{\hrule height.2ex width.3em}\hskip0.1em}
a931f1b45151 new style file
lcp
parents:
diff changeset
    66
a931f1b45151 new style file
lcp
parents:
diff changeset
    67
%%% \dquotes permits usage of "..." for \hbox{...} -- also taken from under.sty
a931f1b45151 new style file
lcp
parents:
diff changeset
    68
{\catcode`\"=\active
a931f1b45151 new style file
lcp
parents:
diff changeset
    69
\gdef\dquotes{\catcode`\"=\active  \let"=\@mathText}%
a931f1b45151 new style file
lcp
parents:
diff changeset
    70
\gdef\@mathText#1"{\hbox{\mathTextFont #1\/}}}
a931f1b45151 new style file
lcp
parents:
diff changeset
    71
\def\mathTextFont{\frenchspacing\tt}
6123
4ba5066d01fc defined dquotesoff
paulson
parents: 5765
diff changeset
    72
\def\dquotesoff{\catcode`\"=\other}
110
a931f1b45151 new style file
lcp
parents:
diff changeset
    73
a931f1b45151 new style file
lcp
parents:
diff changeset
    74
%%%% meta-logical connectives
a931f1b45151 new style file
lcp
parents:
diff changeset
    75
a931f1b45151 new style file
lcp
parents:
diff changeset
    76
\let\Forall=\bigwedge
a931f1b45151 new style file
lcp
parents:
diff changeset
    77
\let\Imp=\Longrightarrow
a931f1b45151 new style file
lcp
parents:
diff changeset
    78
\let\To=\Rightarrow
a931f1b45151 new style file
lcp
parents:
diff changeset
    79
\newcommand\Var[1]{{?\!#1}}
5765
wenzelm
parents: 5752
diff changeset
    80
\newcommand\All[1]{\Forall#1.}  %quantification
110
a931f1b45151 new style file
lcp
parents:
diff changeset
    81
a931f1b45151 new style file
lcp
parents:
diff changeset
    82
%%%% ``WARNING'' environment
a931f1b45151 new style file
lcp
parents:
diff changeset
    83
\def\dbend{\vtop to 0pt{\vss\hbox{\Huge\bf!}\vss}}
a931f1b45151 new style file
lcp
parents:
diff changeset
    84
\newenvironment{warn}{\medskip\medbreak\begingroup \clubpenalty=10000 
293
63a0077dd9f2 first draft of Springer volume
lcp
parents: 140
diff changeset
    85
         \small %%WAS\baselineskip=0.9\baselineskip
63a0077dd9f2 first draft of Springer volume
lcp
parents: 140
diff changeset
    86
         \noindent \hangindent\parindent \hangafter=-2 
63a0077dd9f2 first draft of Springer volume
lcp
parents: 140
diff changeset
    87
         \hbox to0pt{\hskip-\hangindent\dbend\hfill}\ignorespaces}%
63a0077dd9f2 first draft of Springer volume
lcp
parents: 140
diff changeset
    88
        {\par\endgroup\medbreak}
110
a931f1b45151 new style file
lcp
parents:
diff changeset
    89
a931f1b45151 new style file
lcp
parents:
diff changeset
    90
a931f1b45151 new style file
lcp
parents:
diff changeset
    91
%%%% Standard logical symbols
a931f1b45151 new style file
lcp
parents:
diff changeset
    92
\let\turn=\vdash
a931f1b45151 new style file
lcp
parents:
diff changeset
    93
\let\conj=\wedge
a931f1b45151 new style file
lcp
parents:
diff changeset
    94
\let\disj=\vee
a931f1b45151 new style file
lcp
parents:
diff changeset
    95
\let\imp=\rightarrow
a931f1b45151 new style file
lcp
parents:
diff changeset
    96
\let\bimp=\leftrightarrow
293
63a0077dd9f2 first draft of Springer volume
lcp
parents: 140
diff changeset
    97
\newcommand\all[1]{\forall#1.}  %quantification
110
a931f1b45151 new style file
lcp
parents:
diff changeset
    98
\newcommand\ex[1]{\exists#1.}
a931f1b45151 new style file
lcp
parents:
diff changeset
    99
\newcommand{\pair}[1]{\langle#1\rangle}
a931f1b45151 new style file
lcp
parents:
diff changeset
   100
5752
c3df312f34a2 matharray;
wenzelm
parents: 4244
diff changeset
   101
\newcommand{\lparr}{\mathopen{(\!|}}
c3df312f34a2 matharray;
wenzelm
parents: 4244
diff changeset
   102
\newcommand{\rparr}{\mathclose{|\!)}}
c3df312f34a2 matharray;
wenzelm
parents: 4244
diff changeset
   103
\newcommand{\fs}{\mathpunct{,\,}}
c3df312f34a2 matharray;
wenzelm
parents: 4244
diff changeset
   104
\newcommand{\ty}{\mathrel{::}}
c3df312f34a2 matharray;
wenzelm
parents: 4244
diff changeset
   105
\newcommand{\asn}{\mathrel{:=}}
c3df312f34a2 matharray;
wenzelm
parents: 4244
diff changeset
   106
\newcommand{\more}{\ldots}
c3df312f34a2 matharray;
wenzelm
parents: 4244
diff changeset
   107
\newcommand{\record}[1]{\lparr #1 \rparr}
5765
wenzelm
parents: 5752
diff changeset
   108
\newcommand{\dtt}{\mathord.}
5752
c3df312f34a2 matharray;
wenzelm
parents: 4244
diff changeset
   109
110
a931f1b45151 new style file
lcp
parents:
diff changeset
   110
\newcommand\lbrakk{\mathopen{[\![}}
a931f1b45151 new style file
lcp
parents:
diff changeset
   111
\newcommand\rbrakk{\mathclose{]\!]}}
a931f1b45151 new style file
lcp
parents:
diff changeset
   112
\newcommand\List[1]{\lbrakk#1\rbrakk}  %was \obj
a931f1b45151 new style file
lcp
parents:
diff changeset
   113
\newcommand\vpile[1]{\begin{array}{c}#1\end{array}}
5752
c3df312f34a2 matharray;
wenzelm
parents: 4244
diff changeset
   114
\newenvironment{matharray}[1]{\[\begin{array}{#1}}{\end{array}\]}
7139
1af4c1f48368 added \text;
wenzelm
parents: 7043
diff changeset
   115
\newcommand{\text}[1]{\mbox{#1}}
110
a931f1b45151 new style file
lcp
parents:
diff changeset
   116
a931f1b45151 new style file
lcp
parents:
diff changeset
   117
\let\int=\cap
a931f1b45151 new style file
lcp
parents:
diff changeset
   118
\let\un=\cup
a931f1b45151 new style file
lcp
parents:
diff changeset
   119
\let\inter=\bigcap
a931f1b45151 new style file
lcp
parents:
diff changeset
   120
\let\union=\bigcup
a931f1b45151 new style file
lcp
parents:
diff changeset
   121
a931f1b45151 new style file
lcp
parents:
diff changeset
   122
\def\ML{{\sc ml}}
a931f1b45151 new style file
lcp
parents:
diff changeset
   123
\def\OBJ{{\sc obj}}
350
d9ebca601847 post-CRC corrections
lcp
parents: 301
diff changeset
   124
\def\AST{{\sc ast}}
110
a931f1b45151 new style file
lcp
parents:
diff changeset
   125
3109
d95748813188 added \Pure, \CPure;
wenzelm
parents: 3100
diff changeset
   126
\def\Pure{{\tt Pure}\@}
d95748813188 added \Pure, \CPure;
wenzelm
parents: 3100
diff changeset
   127
\def\CPure{{\tt CPure}\@}
110
a931f1b45151 new style file
lcp
parents:
diff changeset
   128
\def\LCF{{\tt LCF}\@}
a931f1b45151 new style file
lcp
parents:
diff changeset
   129
\def\FOL{{\tt FOL}\@}
a931f1b45151 new style file
lcp
parents:
diff changeset
   130
\def\HOL{{\tt HOL}\@}
1648
60ded8c1748c Messed up last update.
nipkow
parents: 1647
diff changeset
   131
\def\HOLCF{{\tt HOLCF}\@}
110
a931f1b45151 new style file
lcp
parents:
diff changeset
   132
\def\LK{{\tt LK}\@}
a931f1b45151 new style file
lcp
parents:
diff changeset
   133
\def\ZF{{\tt ZF}\@}
a931f1b45151 new style file
lcp
parents:
diff changeset
   134
\def\CTT{{\tt CTT}\@}
3109
d95748813188 added \Pure, \CPure;
wenzelm
parents: 3100
diff changeset
   135
\def\Cube{{\tt Cube}\@}
d95748813188 added \Pure, \CPure;
wenzelm
parents: 3100
diff changeset
   136
\def\Modal{{\tt Modal}\@}
110
a931f1b45151 new style file
lcp
parents:
diff changeset
   137
a931f1b45151 new style file
lcp
parents:
diff changeset
   138
%macros to change the treatment of symbols
a931f1b45151 new style file
lcp
parents:
diff changeset
   139
\def\relsemicolon{\mathcode`\;="303B}   %treat ; like a relation
a931f1b45151 new style file
lcp
parents:
diff changeset
   140
\def\binperiod{\mathcode`\.="213A}   %treat . like a binary operator
a931f1b45151 new style file
lcp
parents:
diff changeset
   141
\def\binvert{\mathcode`\|="226A}     %treat | like a binary operator
a931f1b45151 new style file
lcp
parents:
diff changeset
   142
a931f1b45151 new style file
lcp
parents:
diff changeset
   143
%redefinition of \sloppy and \fussy to use \emergencystretch
a931f1b45151 new style file
lcp
parents:
diff changeset
   144
\def\sloppy{\tolerance2000 \hfuzz.5pt \vfuzz.5pt \emergencystretch=15pt}
a931f1b45151 new style file
lcp
parents:
diff changeset
   145
\def\fussy{\tolerance200 \hfuzz.1pt \vfuzz.1pt \emergencystretch=0pt}
a931f1b45151 new style file
lcp
parents:
diff changeset
   146
350
d9ebca601847 post-CRC corrections
lcp
parents: 301
diff changeset
   147
%%%% \tt things
d9ebca601847 post-CRC corrections
lcp
parents: 301
diff changeset
   148
d9ebca601847 post-CRC corrections
lcp
parents: 301
diff changeset
   149
\def\ttdescriptionlabel#1{\hspace\labelsep \tt #1}
d9ebca601847 post-CRC corrections
lcp
parents: 301
diff changeset
   150
\def\ttdescription{\list{}{\labelwidth\z@ \itemindent-\leftmargin
d9ebca601847 post-CRC corrections
lcp
parents: 301
diff changeset
   151
       \let\makelabel\ttdescriptionlabel}}
d9ebca601847 post-CRC corrections
lcp
parents: 301
diff changeset
   152
d9ebca601847 post-CRC corrections
lcp
parents: 301
diff changeset
   153
\let\endttdescription\endlist
d9ebca601847 post-CRC corrections
lcp
parents: 301
diff changeset
   154
293
63a0077dd9f2 first draft of Springer volume
lcp
parents: 140
diff changeset
   155
\chardef\ttilde=`\~     % A tilde for \tt font
63a0077dd9f2 first draft of Springer volume
lcp
parents: 140
diff changeset
   156
\chardef\ttback=`\\     % A backslash for \tt font
63a0077dd9f2 first draft of Springer volume
lcp
parents: 140
diff changeset
   157
\chardef\ttlbrace=`\{   % A left brace for \tt font
63a0077dd9f2 first draft of Springer volume
lcp
parents: 140
diff changeset
   158
\chardef\ttrbrace=`\}   % A right brace for \tt font
110
a931f1b45151 new style file
lcp
parents:
diff changeset
   159
4244
f50dace8be9f New, higher-level definition of \\out macro
paulson
parents: 3491
diff changeset
   160
\newcommand\out{\ \ttfamily\slshape}   %% for output from terminal sessions
110
a931f1b45151 new style file
lcp
parents:
diff changeset
   161
a931f1b45151 new style file
lcp
parents:
diff changeset
   162
% The mathcodes for the letters A, ..., Z, a, ..., z are changed to
140
3a8c68d1d466 changed itmath trickery to be compatible with NFSS (itmath.sty)
nipkow
parents: 110
diff changeset
   163
% generate text italic rather than math italic by default. This makes
110
a931f1b45151 new style file
lcp
parents:
diff changeset
   164
% multi-letter identifiers look better. The mathcode for character c
3096
ccc2c92bb232 Updated to LaTeX 2e
berghofe
parents: 1648
diff changeset
   165
% is set to |"7000| (variable family) + |"400| (text italic) + |c|.
140
3a8c68d1d466 changed itmath trickery to be compatible with NFSS (itmath.sty)
nipkow
parents: 110
diff changeset
   166
%
3096
ccc2c92bb232 Updated to LaTeX 2e
berghofe
parents: 1648
diff changeset
   167
\DeclareSymbolFont{italics}{\encodingdefault}{\rmdefault}{m}{it}%
110
a931f1b45151 new style file
lcp
parents:
diff changeset
   168
\def\@setmcodes#1#2#3{{\count0=#1 \count1=#3
140
3a8c68d1d466 changed itmath trickery to be compatible with NFSS (itmath.sty)
nipkow
parents: 110
diff changeset
   169
        \loop \global\mathcode\count0=\count1 \ifnum \count0<#2
3a8c68d1d466 changed itmath trickery to be compatible with NFSS (itmath.sty)
nipkow
parents: 110
diff changeset
   170
        \advance\count0 by1 \advance\count1 by1 \repeat}}
3096
ccc2c92bb232 Updated to LaTeX 2e
berghofe
parents: 1648
diff changeset
   171
\@setmcodes{`A}{`Z}{"7\hexnumber@\symitalics41}
ccc2c92bb232 Updated to LaTeX 2e
berghofe
parents: 1648
diff changeset
   172
\@setmcodes{`a}{`z}{"7\hexnumber@\symitalics61}