doc-src/iman.sty
author paulson
Fri, 17 Jan 1997 12:49:31 +0100
changeset 2516 4d68fbe6378b
parent 1648 60ded8c1748c
child 3096 ccc2c92bb232
permissions -rw-r--r--
Now with Andy Gordon's treatment of freshness to replace newN/K
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
a931f1b45151 new style file
lcp
parents:
diff changeset
    16
\newcommand\bold[1]{{\bf#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}}
d9ebca601847 post-CRC corrections
lcp
parents: 301
diff changeset
    34
\newcommand\tydx[1]{{\tt#1}\index{#1@{\tt#1} type}}
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
110
a931f1b45151 new style file
lcp
parents:
diff changeset
    37
%for cross-references: 2nd argument (page number) is ignored
a931f1b45151 new style file
lcp
parents:
diff changeset
    38
\newcommand\see[2]{{\it see \/}{#1}}
a931f1b45151 new style file
lcp
parents:
diff changeset
    39
\newcommand\seealso[2]{{\it see also \/}{#1}}
a931f1b45151 new style file
lcp
parents:
diff changeset
    40
a931f1b45151 new style file
lcp
parents:
diff changeset
    41
%set argument in \tt font; at the sime time, index using * prefix
350
d9ebca601847 post-CRC corrections
lcp
parents: 301
diff changeset
    42
\newcommand\rmindex[1]{{#1}\index{#1}\@}
110
a931f1b45151 new style file
lcp
parents:
diff changeset
    43
\newcommand\ttindex[1]{{\tt#1}\index{*#1}\@}
a931f1b45151 new style file
lcp
parents:
diff changeset
    44
\newcommand\ttindexbold[1]{{\tt#1}\index{*#1|bold}\@}
a931f1b45151 new style file
lcp
parents:
diff changeset
    45
a931f1b45151 new style file
lcp
parents:
diff changeset
    46
%set argument in \bf font and index in ROMAN font (for definitions in text!)
a931f1b45151 new style file
lcp
parents:
diff changeset
    47
\newcommand\bfindex[1]{{\bf#1}\index{#1|bold}\@}
a931f1b45151 new style file
lcp
parents:
diff changeset
    48
a931f1b45151 new style file
lcp
parents:
diff changeset
    49
a931f1b45151 new style file
lcp
parents:
diff changeset
    50
%%% underscores as ordinary characters, not for subscripting
a931f1b45151 new style file
lcp
parents:
diff changeset
    51
%%  use @ or \sb for subscripting; use \at for @
a931f1b45151 new style file
lcp
parents:
diff changeset
    52
%%  only works in \tt font
a931f1b45151 new style file
lcp
parents:
diff changeset
    53
%%  must not make _ an active char; would make \ttindex fail!
a931f1b45151 new style file
lcp
parents:
diff changeset
    54
\gdef\underscoreoff{\catcode`\@=8\catcode`\_=\other}
a931f1b45151 new style file
lcp
parents:
diff changeset
    55
\gdef\underscoreon{\catcode`\_=8\makeatother}
a931f1b45151 new style file
lcp
parents:
diff changeset
    56
\chardef\other=12
a931f1b45151 new style file
lcp
parents:
diff changeset
    57
\chardef\at=`\@
a931f1b45151 new style file
lcp
parents:
diff changeset
    58
a931f1b45151 new style file
lcp
parents:
diff changeset
    59
% alternative underscore
a931f1b45151 new style file
lcp
parents:
diff changeset
    60
\def\_{\leavevmode\kern.06em\vbox{\hrule height.2ex width.3em}\hskip0.1em}
a931f1b45151 new style file
lcp
parents:
diff changeset
    61
a931f1b45151 new style file
lcp
parents:
diff changeset
    62
%%% \dquotes permits usage of "..." for \hbox{...} -- also taken from under.sty
a931f1b45151 new style file
lcp
parents:
diff changeset
    63
{\catcode`\"=\active
a931f1b45151 new style file
lcp
parents:
diff changeset
    64
\gdef\dquotes{\catcode`\"=\active  \let"=\@mathText}%
a931f1b45151 new style file
lcp
parents:
diff changeset
    65
\gdef\@mathText#1"{\hbox{\mathTextFont #1\/}}}
a931f1b45151 new style file
lcp
parents:
diff changeset
    66
\def\mathTextFont{\frenchspacing\tt}
a931f1b45151 new style file
lcp
parents:
diff changeset
    67
a931f1b45151 new style file
lcp
parents:
diff changeset
    68
%%%% meta-logical connectives
a931f1b45151 new style file
lcp
parents:
diff changeset
    69
a931f1b45151 new style file
lcp
parents:
diff changeset
    70
\let\Forall=\bigwedge
a931f1b45151 new style file
lcp
parents:
diff changeset
    71
\let\Imp=\Longrightarrow
a931f1b45151 new style file
lcp
parents:
diff changeset
    72
\let\To=\Rightarrow
a931f1b45151 new style file
lcp
parents:
diff changeset
    73
\newcommand\Var[1]{{?\!#1}}
a931f1b45151 new style file
lcp
parents:
diff changeset
    74
a931f1b45151 new style file
lcp
parents:
diff changeset
    75
%%%% ``WARNING'' environment
a931f1b45151 new style file
lcp
parents:
diff changeset
    76
\def\dbend{\vtop to 0pt{\vss\hbox{\Huge\bf!}\vss}}
a931f1b45151 new style file
lcp
parents:
diff changeset
    77
\newenvironment{warn}{\medskip\medbreak\begingroup \clubpenalty=10000 
293
63a0077dd9f2 first draft of Springer volume
lcp
parents: 140
diff changeset
    78
         \small %%WAS\baselineskip=0.9\baselineskip
63a0077dd9f2 first draft of Springer volume
lcp
parents: 140
diff changeset
    79
         \noindent \hangindent\parindent \hangafter=-2 
63a0077dd9f2 first draft of Springer volume
lcp
parents: 140
diff changeset
    80
         \hbox to0pt{\hskip-\hangindent\dbend\hfill}\ignorespaces}%
63a0077dd9f2 first draft of Springer volume
lcp
parents: 140
diff changeset
    81
        {\par\endgroup\medbreak}
110
a931f1b45151 new style file
lcp
parents:
diff changeset
    82
a931f1b45151 new style file
lcp
parents:
diff changeset
    83
a931f1b45151 new style file
lcp
parents:
diff changeset
    84
%%%% Standard logical symbols
a931f1b45151 new style file
lcp
parents:
diff changeset
    85
\let\turn=\vdash
a931f1b45151 new style file
lcp
parents:
diff changeset
    86
\let\conj=\wedge
a931f1b45151 new style file
lcp
parents:
diff changeset
    87
\let\disj=\vee
a931f1b45151 new style file
lcp
parents:
diff changeset
    88
\let\imp=\rightarrow
a931f1b45151 new style file
lcp
parents:
diff changeset
    89
\let\bimp=\leftrightarrow
293
63a0077dd9f2 first draft of Springer volume
lcp
parents: 140
diff changeset
    90
\newcommand\all[1]{\forall#1.}  %quantification
110
a931f1b45151 new style file
lcp
parents:
diff changeset
    91
\newcommand\ex[1]{\exists#1.}
a931f1b45151 new style file
lcp
parents:
diff changeset
    92
\newcommand{\pair}[1]{\langle#1\rangle}
a931f1b45151 new style file
lcp
parents:
diff changeset
    93
a931f1b45151 new style file
lcp
parents:
diff changeset
    94
\newcommand\lbrakk{\mathopen{[\![}}
a931f1b45151 new style file
lcp
parents:
diff changeset
    95
\newcommand\rbrakk{\mathclose{]\!]}}
a931f1b45151 new style file
lcp
parents:
diff changeset
    96
\newcommand\List[1]{\lbrakk#1\rbrakk}  %was \obj
a931f1b45151 new style file
lcp
parents:
diff changeset
    97
\newcommand\vpile[1]{\begin{array}{c}#1\end{array}}
a931f1b45151 new style file
lcp
parents:
diff changeset
    98
a931f1b45151 new style file
lcp
parents:
diff changeset
    99
\let\int=\cap
a931f1b45151 new style file
lcp
parents:
diff changeset
   100
\let\un=\cup
a931f1b45151 new style file
lcp
parents:
diff changeset
   101
\let\inter=\bigcap
a931f1b45151 new style file
lcp
parents:
diff changeset
   102
\let\union=\bigcup
a931f1b45151 new style file
lcp
parents:
diff changeset
   103
a931f1b45151 new style file
lcp
parents:
diff changeset
   104
\def\ML{{\sc ml}}
a931f1b45151 new style file
lcp
parents:
diff changeset
   105
\def\OBJ{{\sc obj}}
350
d9ebca601847 post-CRC corrections
lcp
parents: 301
diff changeset
   106
\def\AST{{\sc ast}}
110
a931f1b45151 new style file
lcp
parents:
diff changeset
   107
a931f1b45151 new style file
lcp
parents:
diff changeset
   108
\def\LCF{{\tt LCF}\@}
a931f1b45151 new style file
lcp
parents:
diff changeset
   109
\def\FOL{{\tt FOL}\@}
a931f1b45151 new style file
lcp
parents:
diff changeset
   110
\def\HOL{{\tt HOL}\@}
1648
60ded8c1748c Messed up last update.
nipkow
parents: 1647
diff changeset
   111
\def\HOLCF{{\tt HOLCF}\@}
110
a931f1b45151 new style file
lcp
parents:
diff changeset
   112
\def\LK{{\tt LK}\@}
a931f1b45151 new style file
lcp
parents:
diff changeset
   113
\def\ZF{{\tt ZF}\@}
a931f1b45151 new style file
lcp
parents:
diff changeset
   114
\def\CTT{{\tt CTT}\@}
a931f1b45151 new style file
lcp
parents:
diff changeset
   115
\def\Cube{{\tt Cube}}
a931f1b45151 new style file
lcp
parents:
diff changeset
   116
\def\Modal{{\tt Modal}}
a931f1b45151 new style file
lcp
parents:
diff changeset
   117
a931f1b45151 new style file
lcp
parents:
diff changeset
   118
%macros to change the treatment of symbols
a931f1b45151 new style file
lcp
parents:
diff changeset
   119
\def\relsemicolon{\mathcode`\;="303B}   %treat ; like a relation
a931f1b45151 new style file
lcp
parents:
diff changeset
   120
\def\binperiod{\mathcode`\.="213A}   %treat . like a binary operator
a931f1b45151 new style file
lcp
parents:
diff changeset
   121
\def\binvert{\mathcode`\|="226A}     %treat | like a binary operator
a931f1b45151 new style file
lcp
parents:
diff changeset
   122
a931f1b45151 new style file
lcp
parents:
diff changeset
   123
%redefinition of \sloppy and \fussy to use \emergencystretch
a931f1b45151 new style file
lcp
parents:
diff changeset
   124
\def\sloppy{\tolerance2000 \hfuzz.5pt \vfuzz.5pt \emergencystretch=15pt}
a931f1b45151 new style file
lcp
parents:
diff changeset
   125
\def\fussy{\tolerance200 \hfuzz.1pt \vfuzz.1pt \emergencystretch=0pt}
a931f1b45151 new style file
lcp
parents:
diff changeset
   126
350
d9ebca601847 post-CRC corrections
lcp
parents: 301
diff changeset
   127
%%%% \tt things
d9ebca601847 post-CRC corrections
lcp
parents: 301
diff changeset
   128
d9ebca601847 post-CRC corrections
lcp
parents: 301
diff changeset
   129
\def\ttdescriptionlabel#1{\hspace\labelsep \tt #1}
d9ebca601847 post-CRC corrections
lcp
parents: 301
diff changeset
   130
\def\ttdescription{\list{}{\labelwidth\z@ \itemindent-\leftmargin
d9ebca601847 post-CRC corrections
lcp
parents: 301
diff changeset
   131
       \let\makelabel\ttdescriptionlabel}}
d9ebca601847 post-CRC corrections
lcp
parents: 301
diff changeset
   132
d9ebca601847 post-CRC corrections
lcp
parents: 301
diff changeset
   133
\let\endttdescription\endlist
d9ebca601847 post-CRC corrections
lcp
parents: 301
diff changeset
   134
293
63a0077dd9f2 first draft of Springer volume
lcp
parents: 140
diff changeset
   135
\chardef\ttilde=`\~     % A tilde for \tt font
63a0077dd9f2 first draft of Springer volume
lcp
parents: 140
diff changeset
   136
\chardef\ttback=`\\     % A backslash for \tt font
63a0077dd9f2 first draft of Springer volume
lcp
parents: 140
diff changeset
   137
\chardef\ttlbrace=`\{   % A left brace for \tt font
63a0077dd9f2 first draft of Springer volume
lcp
parents: 140
diff changeset
   138
\chardef\ttrbrace=`\}   % A right brace for \tt font
110
a931f1b45151 new style file
lcp
parents:
diff changeset
   139
a931f1b45151 new style file
lcp
parents:
diff changeset
   140
\newfont{\sltt}{cmsltt10}     %% for output from terminal sessions
a931f1b45151 new style file
lcp
parents:
diff changeset
   141
\newcommand\out{\ \sltt}
a931f1b45151 new style file
lcp
parents:
diff changeset
   142
140
3a8c68d1d466 changed itmath trickery to be compatible with NFSS (itmath.sty)
nipkow
parents: 110
diff changeset
   143
% "itmath.sty" use cmr italic for letters in math mode and get the
293
63a0077dd9f2 first draft of Springer volume
lcp
parents: 140
diff changeset
   144
%              usual letter spacing of text mode.
140
3a8c68d1d466 changed itmath trickery to be compatible with NFSS (itmath.sty)
nipkow
parents: 110
diff changeset
   145
%
3a8c68d1d466 changed itmath trickery to be compatible with NFSS (itmath.sty)
nipkow
parents: 110
diff changeset
   146
% Michael Lawley, April 1993
3a8c68d1d466 changed itmath trickery to be compatible with NFSS (itmath.sty)
nipkow
parents: 110
diff changeset
   147
% (lawley@cit.gu.edu.au)
3a8c68d1d466 changed itmath trickery to be compatible with NFSS (itmath.sty)
nipkow
parents: 110
diff changeset
   148
%
3a8c68d1d466 changed itmath trickery to be compatible with NFSS (itmath.sty)
nipkow
parents: 110
diff changeset
   149
% Derived from itma.sty (of unknown origin).
110
a931f1b45151 new style file
lcp
parents:
diff changeset
   150
%
a931f1b45151 new style file
lcp
parents:
diff changeset
   151
% MATHCODES
a931f1b45151 new style file
lcp
parents:
diff changeset
   152
%
a931f1b45151 new style file
lcp
parents:
diff changeset
   153
% 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
   154
% generate text italic rather than math italic by default. This makes
110
a931f1b45151 new style file
lcp
parents:
diff changeset
   155
% multi-letter identifiers look better. The mathcode for character c
140
3a8c68d1d466 changed itmath trickery to be compatible with NFSS (itmath.sty)
nipkow
parents: 110
diff changeset
   156
% is set to "7000 (variable class) + "400 (text italic) + c.
3a8c68d1d466 changed itmath trickery to be compatible with NFSS (itmath.sty)
nipkow
parents: 110
diff changeset
   157
%
3a8c68d1d466 changed itmath trickery to be compatible with NFSS (itmath.sty)
nipkow
parents: 110
diff changeset
   158
% For NFSS the mathcode is "7000 (variable class) + (hex)\itfam + c
3a8c68d1d466 changed itmath trickery to be compatible with NFSS (itmath.sty)
nipkow
parents: 110
diff changeset
   159
% \itfam is probably equal to 7.
3a8c68d1d466 changed itmath trickery to be compatible with NFSS (itmath.sty)
nipkow
parents: 110
diff changeset
   160
%
3a8c68d1d466 changed itmath trickery to be compatible with NFSS (itmath.sty)
nipkow
parents: 110
diff changeset
   161
3a8c68d1d466 changed itmath trickery to be compatible with NFSS (itmath.sty)
nipkow
parents: 110
diff changeset
   162
\ifx\undefined\hexnumber@
3a8c68d1d466 changed itmath trickery to be compatible with NFSS (itmath.sty)
nipkow
parents: 110
diff changeset
   163
  \def\hexnumber@#1{\ifcase#1 \z@
3a8c68d1d466 changed itmath trickery to be compatible with NFSS (itmath.sty)
nipkow
parents: 110
diff changeset
   164
  \or \@ne \or \tw@ \or \thr@@
3a8c68d1d466 changed itmath trickery to be compatible with NFSS (itmath.sty)
nipkow
parents: 110
diff changeset
   165
  \or 4\or 5\or 6\or 7\or 8\or
3a8c68d1d466 changed itmath trickery to be compatible with NFSS (itmath.sty)
nipkow
parents: 110
diff changeset
   166
  9\or A\or B\or C\or D\or E\or F\fi}
3a8c68d1d466 changed itmath trickery to be compatible with NFSS (itmath.sty)
nipkow
parents: 110
diff changeset
   167
\fi
110
a931f1b45151 new style file
lcp
parents:
diff changeset
   168
a931f1b45151 new style file
lcp
parents:
diff changeset
   169
\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
   170
        \loop \global\mathcode\count0=\count1 \ifnum \count0<#2
3a8c68d1d466 changed itmath trickery to be compatible with NFSS (itmath.sty)
nipkow
parents: 110
diff changeset
   171
        \advance\count0 by1 \advance\count1 by1 \repeat}}
3a8c68d1d466 changed itmath trickery to be compatible with NFSS (itmath.sty)
nipkow
parents: 110
diff changeset
   172
3a8c68d1d466 changed itmath trickery to be compatible with NFSS (itmath.sty)
nipkow
parents: 110
diff changeset
   173
\edef\@tempa{\hexnumber@\itfam}
110
a931f1b45151 new style file
lcp
parents:
diff changeset
   174
140
3a8c68d1d466 changed itmath trickery to be compatible with NFSS (itmath.sty)
nipkow
parents: 110
diff changeset
   175
\@setmcodes{`A}{`Z}{"7\@tempa 41}
3a8c68d1d466 changed itmath trickery to be compatible with NFSS (itmath.sty)
nipkow
parents: 110
diff changeset
   176
\@setmcodes{`a}{`z}{"7\@tempa 61}
3a8c68d1d466 changed itmath trickery to be compatible with NFSS (itmath.sty)
nipkow
parents: 110
diff changeset
   177
3a8c68d1d466 changed itmath trickery to be compatible with NFSS (itmath.sty)
nipkow
parents: 110
diff changeset
   178
\ifx\define@mathgroup\undefined\else
293
63a0077dd9f2 first draft of Springer volume
lcp
parents: 140
diff changeset
   179
        \define@mathgroup\mv@normal{\itfam}{cmr}{m}{it}\fi