doc-src/iman.sty
author paulson
Tue, 10 Feb 2004 12:02:11 +0100
changeset 14378 69c4d5997669
parent 10092 4295180d6bab
child 39860 788e902f3c59
permissions -rw-r--r--
generic of_nat and of_int functions, and generalization of iszero and neg
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
8827
5c5c68f4610d \usepackage{makeidx};
wenzelm
parents: 7976
diff changeset
    15
10092
4295180d6bab exchanged the declaration of "seealso" and loading of "makeidx" because the
paulson
parents: 9693
diff changeset
    16
\newcommand\seealso[2]{\emph{see also} #1}
8827
5c5c68f4610d \usepackage{makeidx};
wenzelm
parents: 7976
diff changeset
    17
\usepackage{makeidx}
5c5c68f4610d \usepackage{makeidx};
wenzelm
parents: 7976
diff changeset
    18
110
a931f1b45151 new style file
lcp
parents:
diff changeset
    19
%index, putting page numbers of definitions in boldface
6747
cee5adcc1f5c \def\bold;
wenzelm
parents: 6123
diff changeset
    20
\def\bold#1{\textbf{#1}}
293
63a0077dd9f2 first draft of Springer volume
lcp
parents: 140
diff changeset
    21
\newcommand\fnote[1]{#1n}
110
a931f1b45151 new style file
lcp
parents:
diff changeset
    22
\newcommand\indexbold[1]{\index{#1|bold}}
a931f1b45151 new style file
lcp
parents:
diff changeset
    23
350
d9ebca601847 post-CRC corrections
lcp
parents: 301
diff changeset
    24
%for indexing constants, symbols, theorems, ...
d9ebca601847 post-CRC corrections
lcp
parents: 301
diff changeset
    25
\newcommand\cdx[1]{{\tt#1}\index{#1@{\tt#1} constant}}
d9ebca601847 post-CRC corrections
lcp
parents: 301
diff changeset
    26
\newcommand\sdx[1]{{\tt#1}\index{#1@{\tt#1} symbol}}
d9ebca601847 post-CRC corrections
lcp
parents: 301
diff changeset
    27
d9ebca601847 post-CRC corrections
lcp
parents: 301
diff changeset
    28
\newcommand\tdx[1]{{\tt#1}\index{#1@{\tt#1} theorem}}
d9ebca601847 post-CRC corrections
lcp
parents: 301
diff changeset
    29
\newcommand\tdxbold[1]{{\tt#1}\index{#1@{\tt#1} theorem|bold}}
d9ebca601847 post-CRC corrections
lcp
parents: 301
diff changeset
    30
d9ebca601847 post-CRC corrections
lcp
parents: 301
diff changeset
    31
\newcommand\mltydx[1]{{\tt#1}\index{#1@{\tt#1} ML type}}
d9ebca601847 post-CRC corrections
lcp
parents: 301
diff changeset
    32
\newcommand\xdx[1]{{\tt#1}\index{#1@{\tt#1} exception}}
d9ebca601847 post-CRC corrections
lcp
parents: 301
diff changeset
    33
d9ebca601847 post-CRC corrections
lcp
parents: 301
diff changeset
    34
\newcommand\ndx[1]{{\tt#1}\index{#1@{\tt#1} nonterminal}}
d9ebca601847 post-CRC corrections
lcp
parents: 301
diff changeset
    35
\newcommand\ndxbold[1]{{\tt#1}\index{#1@{\tt#1} nonterminal|bold}}
d9ebca601847 post-CRC corrections
lcp
parents: 301
diff changeset
    36
d9ebca601847 post-CRC corrections
lcp
parents: 301
diff changeset
    37
\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
    38
\newcommand\tydx[1]{\textit{#1}\index{#1@{\textit{#1}} type}}
350
d9ebca601847 post-CRC corrections
lcp
parents: 301
diff changeset
    39
\newcommand\thydx[1]{{\tt#1}\index{#1@{\tt#1} theory}}
d9ebca601847 post-CRC corrections
lcp
parents: 301
diff changeset
    40
3187
8f8c88dcd728 added \tooldx;
wenzelm
parents: 3109
diff changeset
    41
\newcommand\tooldx[1]{{\tt#1}\index{#1@{\tt#1} tool}}
3211
57a9b613036e added \settdx;
wenzelm
parents: 3187
diff changeset
    42
\newcommand\settdx[1]{{\tt#1}\index{#1@{\tt#1} setting}}
3187
8f8c88dcd728 added \tooldx;
wenzelm
parents: 3109
diff changeset
    43
3100
2b0f9ff06018 fixed comment;
wenzelm
parents: 3096
diff changeset
    44
%set argument in \tt font; at the same time, index using * prefix
350
d9ebca601847 post-CRC corrections
lcp
parents: 301
diff changeset
    45
\newcommand\rmindex[1]{{#1}\index{#1}\@}
110
a931f1b45151 new style file
lcp
parents:
diff changeset
    46
\newcommand\ttindex[1]{{\tt#1}\index{*#1}\@}
a931f1b45151 new style file
lcp
parents:
diff changeset
    47
\newcommand\ttindexbold[1]{{\tt#1}\index{*#1|bold}\@}
a931f1b45151 new style file
lcp
parents:
diff changeset
    48
a931f1b45151 new style file
lcp
parents:
diff changeset
    49
%set argument in \bf font and index in ROMAN font (for definitions in text!)
a931f1b45151 new style file
lcp
parents:
diff changeset
    50
\newcommand\bfindex[1]{{\bf#1}\index{#1|bold}\@}
a931f1b45151 new style file
lcp
parents:
diff changeset
    51
a931f1b45151 new style file
lcp
parents:
diff changeset
    52
a931f1b45151 new style file
lcp
parents:
diff changeset
    53
%%% underscores as ordinary characters, not for subscripting
a931f1b45151 new style file
lcp
parents:
diff changeset
    54
%%  use @ or \sb for subscripting; use \at for @
a931f1b45151 new style file
lcp
parents:
diff changeset
    55
%%  only works in \tt font
a931f1b45151 new style file
lcp
parents:
diff changeset
    56
%%  must not make _ an active char; would make \ttindex fail!
a931f1b45151 new style file
lcp
parents:
diff changeset
    57
\gdef\underscoreoff{\catcode`\@=8\catcode`\_=\other}
a931f1b45151 new style file
lcp
parents:
diff changeset
    58
\gdef\underscoreon{\catcode`\_=8\makeatother}
a931f1b45151 new style file
lcp
parents:
diff changeset
    59
\chardef\other=12
a931f1b45151 new style file
lcp
parents:
diff changeset
    60
\chardef\at=`\@
a931f1b45151 new style file
lcp
parents:
diff changeset
    61
a931f1b45151 new style file
lcp
parents:
diff changeset
    62
% alternative underscore
a931f1b45151 new style file
lcp
parents:
diff changeset
    63
\def\_{\leavevmode\kern.06em\vbox{\hrule height.2ex width.3em}\hskip0.1em}
a931f1b45151 new style file
lcp
parents:
diff changeset
    64
a931f1b45151 new style file
lcp
parents:
diff changeset
    65
%%% \dquotes permits usage of "..." for \hbox{...} -- also taken from under.sty
a931f1b45151 new style file
lcp
parents:
diff changeset
    66
{\catcode`\"=\active
a931f1b45151 new style file
lcp
parents:
diff changeset
    67
\gdef\dquotes{\catcode`\"=\active  \let"=\@mathText}%
a931f1b45151 new style file
lcp
parents:
diff changeset
    68
\gdef\@mathText#1"{\hbox{\mathTextFont #1\/}}}
a931f1b45151 new style file
lcp
parents:
diff changeset
    69
\def\mathTextFont{\frenchspacing\tt}
6123
4ba5066d01fc defined dquotesoff
paulson
parents: 5765
diff changeset
    70
\def\dquotesoff{\catcode`\"=\other}
110
a931f1b45151 new style file
lcp
parents:
diff changeset
    71
a931f1b45151 new style file
lcp
parents:
diff changeset
    72
%%%% meta-logical connectives
a931f1b45151 new style file
lcp
parents:
diff changeset
    73
a931f1b45151 new style file
lcp
parents:
diff changeset
    74
\let\Forall=\bigwedge
a931f1b45151 new style file
lcp
parents:
diff changeset
    75
\let\Imp=\Longrightarrow
a931f1b45151 new style file
lcp
parents:
diff changeset
    76
\let\To=\Rightarrow
7455
wenzelm
parents: 7321
diff changeset
    77
\newcommand{\PROP}{\mathop{\mathrm{PROP}}}
wenzelm
parents: 7321
diff changeset
    78
\newcommand{\Var}[1]{{?\!#1}}
wenzelm
parents: 7321
diff changeset
    79
\newcommand{\All}[1]{\Forall#1.}  %quantification
110
a931f1b45151 new style file
lcp
parents:
diff changeset
    80
a931f1b45151 new style file
lcp
parents:
diff changeset
    81
%%%% ``WARNING'' environment
a931f1b45151 new style file
lcp
parents:
diff changeset
    82
\def\dbend{\vtop to 0pt{\vss\hbox{\Huge\bf!}\vss}}
a931f1b45151 new style file
lcp
parents:
diff changeset
    83
\newenvironment{warn}{\medskip\medbreak\begingroup \clubpenalty=10000 
293
63a0077dd9f2 first draft of Springer volume
lcp
parents: 140
diff changeset
    84
         \small %%WAS\baselineskip=0.9\baselineskip
63a0077dd9f2 first draft of Springer volume
lcp
parents: 140
diff changeset
    85
         \noindent \hangindent\parindent \hangafter=-2 
63a0077dd9f2 first draft of Springer volume
lcp
parents: 140
diff changeset
    86
         \hbox to0pt{\hskip-\hangindent\dbend\hfill}\ignorespaces}%
63a0077dd9f2 first draft of Springer volume
lcp
parents: 140
diff changeset
    87
        {\par\endgroup\medbreak}
110
a931f1b45151 new style file
lcp
parents:
diff changeset
    88
a931f1b45151 new style file
lcp
parents:
diff changeset
    89
a931f1b45151 new style file
lcp
parents:
diff changeset
    90
%%%% Standard logical symbols
a931f1b45151 new style file
lcp
parents:
diff changeset
    91
\let\turn=\vdash
a931f1b45151 new style file
lcp
parents:
diff changeset
    92
\let\conj=\wedge
a931f1b45151 new style file
lcp
parents:
diff changeset
    93
\let\disj=\vee
a931f1b45151 new style file
lcp
parents:
diff changeset
    94
\let\imp=\rightarrow
a931f1b45151 new style file
lcp
parents:
diff changeset
    95
\let\bimp=\leftrightarrow
293
63a0077dd9f2 first draft of Springer volume
lcp
parents: 140
diff changeset
    96
\newcommand\all[1]{\forall#1.}  %quantification
110
a931f1b45151 new style file
lcp
parents:
diff changeset
    97
\newcommand\ex[1]{\exists#1.}
a931f1b45151 new style file
lcp
parents:
diff changeset
    98
\newcommand{\pair}[1]{\langle#1\rangle}
a931f1b45151 new style file
lcp
parents:
diff changeset
    99
5752
c3df312f34a2 matharray;
wenzelm
parents: 4244
diff changeset
   100
\newcommand{\lparr}{\mathopen{(\!|}}
c3df312f34a2 matharray;
wenzelm
parents: 4244
diff changeset
   101
\newcommand{\rparr}{\mathclose{|\!)}}
c3df312f34a2 matharray;
wenzelm
parents: 4244
diff changeset
   102
\newcommand{\fs}{\mathpunct{,\,}}
c3df312f34a2 matharray;
wenzelm
parents: 4244
diff changeset
   103
\newcommand{\ty}{\mathrel{::}}
c3df312f34a2 matharray;
wenzelm
parents: 4244
diff changeset
   104
\newcommand{\asn}{\mathrel{:=}}
c3df312f34a2 matharray;
wenzelm
parents: 4244
diff changeset
   105
\newcommand{\more}{\ldots}
c3df312f34a2 matharray;
wenzelm
parents: 4244
diff changeset
   106
\newcommand{\record}[1]{\lparr #1 \rparr}
5765
wenzelm
parents: 5752
diff changeset
   107
\newcommand{\dtt}{\mathord.}
5752
c3df312f34a2 matharray;
wenzelm
parents: 4244
diff changeset
   108
110
a931f1b45151 new style file
lcp
parents:
diff changeset
   109
\newcommand\lbrakk{\mathopen{[\![}}
a931f1b45151 new style file
lcp
parents:
diff changeset
   110
\newcommand\rbrakk{\mathclose{]\!]}}
a931f1b45151 new style file
lcp
parents:
diff changeset
   111
\newcommand\List[1]{\lbrakk#1\rbrakk}  %was \obj
a931f1b45151 new style file
lcp
parents:
diff changeset
   112
\newcommand\vpile[1]{\begin{array}{c}#1\end{array}}
5752
c3df312f34a2 matharray;
wenzelm
parents: 4244
diff changeset
   113
\newenvironment{matharray}[1]{\[\begin{array}{#1}}{\end{array}\]}
9693
a2272ce2316b moved \tt things to ttbox.sty;
wenzelm
parents: 8829
diff changeset
   114
\newcommand{\Text}[1]{\mbox{#1}}
110
a931f1b45151 new style file
lcp
parents:
diff changeset
   115
7976
wenzelm
parents: 7464
diff changeset
   116
\DeclareMathSymbol{\dshsym}{\mathalpha}{letters}{"2D}
wenzelm
parents: 7464
diff changeset
   117
\newcommand{\dsh}{\mathit{\dshsym}}
wenzelm
parents: 7464
diff changeset
   118
110
a931f1b45151 new style file
lcp
parents:
diff changeset
   119
\let\int=\cap
a931f1b45151 new style file
lcp
parents:
diff changeset
   120
\let\un=\cup
a931f1b45151 new style file
lcp
parents:
diff changeset
   121
\let\inter=\bigcap
a931f1b45151 new style file
lcp
parents:
diff changeset
   122
\let\union=\bigcup
a931f1b45151 new style file
lcp
parents:
diff changeset
   123
a931f1b45151 new style file
lcp
parents:
diff changeset
   124
\def\ML{{\sc ml}}
a931f1b45151 new style file
lcp
parents:
diff changeset
   125
\def\OBJ{{\sc obj}}
350
d9ebca601847 post-CRC corrections
lcp
parents: 301
diff changeset
   126
\def\AST{{\sc ast}}
110
a931f1b45151 new style file
lcp
parents:
diff changeset
   127
a931f1b45151 new style file
lcp
parents:
diff changeset
   128
%macros to change the treatment of symbols
a931f1b45151 new style file
lcp
parents:
diff changeset
   129
\def\relsemicolon{\mathcode`\;="303B}   %treat ; like a relation
a931f1b45151 new style file
lcp
parents:
diff changeset
   130
\def\binperiod{\mathcode`\.="213A}   %treat . like a binary operator
a931f1b45151 new style file
lcp
parents:
diff changeset
   131
\def\binvert{\mathcode`\|="226A}     %treat | like a binary operator
a931f1b45151 new style file
lcp
parents:
diff changeset
   132
a931f1b45151 new style file
lcp
parents:
diff changeset
   133
%redefinition of \sloppy and \fussy to use \emergencystretch
a931f1b45151 new style file
lcp
parents:
diff changeset
   134
\def\sloppy{\tolerance2000 \hfuzz.5pt \vfuzz.5pt \emergencystretch=15pt}
a931f1b45151 new style file
lcp
parents:
diff changeset
   135
\def\fussy{\tolerance200 \hfuzz.1pt \vfuzz.1pt \emergencystretch=0pt}
a931f1b45151 new style file
lcp
parents:
diff changeset
   136
7169
76ef91b608a9 tuned attdx, methdx;
wenzelm
parents: 7139
diff changeset
   137
%non-bf version of description
76ef91b608a9 tuned attdx, methdx;
wenzelm
parents: 7139
diff changeset
   138
\def\descrlabel#1{\hspace\labelsep #1}
76ef91b608a9 tuned attdx, methdx;
wenzelm
parents: 7139
diff changeset
   139
\def\descr{\list{}{\labelwidth\z@ \itemindent-\leftmargin\let\makelabel\descrlabel}}
76ef91b608a9 tuned attdx, methdx;
wenzelm
parents: 7139
diff changeset
   140
\let\enddescr\endlist
76ef91b608a9 tuned attdx, methdx;
wenzelm
parents: 7139
diff changeset
   141
110
a931f1b45151 new style file
lcp
parents:
diff changeset
   142
% 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
   143
% generate text italic rather than math italic by default. This makes
110
a931f1b45151 new style file
lcp
parents:
diff changeset
   144
% multi-letter identifiers look better. The mathcode for character c
3096
ccc2c92bb232 Updated to LaTeX 2e
berghofe
parents: 1648
diff changeset
   145
% 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
   146
%
3096
ccc2c92bb232 Updated to LaTeX 2e
berghofe
parents: 1648
diff changeset
   147
\DeclareSymbolFont{italics}{\encodingdefault}{\rmdefault}{m}{it}%
110
a931f1b45151 new style file
lcp
parents:
diff changeset
   148
\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
   149
        \loop \global\mathcode\count0=\count1 \ifnum \count0<#2
3a8c68d1d466 changed itmath trickery to be compatible with NFSS (itmath.sty)
nipkow
parents: 110
diff changeset
   150
        \advance\count0 by1 \advance\count1 by1 \repeat}}
3096
ccc2c92bb232 Updated to LaTeX 2e
berghofe
parents: 1648
diff changeset
   151
\@setmcodes{`A}{`Z}{"7\hexnumber@\symitalics41}
ccc2c92bb232 Updated to LaTeX 2e
berghofe
parents: 1648
diff changeset
   152
\@setmcodes{`a}{`z}{"7\hexnumber@\symitalics61}