|
1 % iman.sty : Isabelle Manual Page Layout |
|
2 % |
|
3 \typeout{Document Style iman. Released 17 February 1994} |
|
4 |
|
5 \hyphenation{Isa-belle man-u-script man-u-scripts ap-pen-dix mut-u-al-ly} |
|
6 \hyphenation{data-type data-types co-data-type co-data-types } |
|
7 |
|
8 \let\ts=\thinspace |
|
9 |
|
10 %usage: \iflabelundefined{LABEL}{if not defined}{if defined} |
|
11 \newcommand{\iflabelundefined}[1]{\@ifundefined{r@#1}} |
|
12 |
|
13 |
|
14 %%%INDEXING use sedindex to process the index |
|
15 |
|
16 \newcommand\seealso[2]{\emph{see also} #1} |
|
17 \usepackage{makeidx} |
|
18 |
|
19 %index, putting page numbers of definitions in boldface |
|
20 \def\bold#1{\textbf{#1}} |
|
21 \newcommand\fnote[1]{#1n} |
|
22 \newcommand\indexbold[1]{\index{#1|bold}} |
|
23 |
|
24 %for indexing constants, symbols, theorems, ... |
|
25 \newcommand\cdx[1]{{\tt#1}\index{#1@{\tt#1} constant}} |
|
26 \newcommand\sdx[1]{{\tt#1}\index{#1@{\tt#1} symbol}} |
|
27 |
|
28 \newcommand\tdx[1]{{\tt#1}\index{#1@{\tt#1} theorem}} |
|
29 \newcommand\tdxbold[1]{{\tt#1}\index{#1@{\tt#1} theorem|bold}} |
|
30 |
|
31 \newcommand\mltydx[1]{{\tt#1}\index{#1@{\tt#1} ML type}} |
|
32 \newcommand\xdx[1]{{\tt#1}\index{#1@{\tt#1} exception}} |
|
33 |
|
34 \newcommand\ndx[1]{{\tt#1}\index{#1@{\tt#1} nonterminal}} |
|
35 \newcommand\ndxbold[1]{{\tt#1}\index{#1@{\tt#1} nonterminal|bold}} |
|
36 |
|
37 \newcommand\cldx[1]{{\tt#1}\index{#1@{\tt#1} class}} |
|
38 \newcommand\tydx[1]{\textit{#1}\index{#1@{\textit{#1}} type}} |
|
39 \newcommand\thydx[1]{{\tt#1}\index{#1@{\tt#1} theory}} |
|
40 |
|
41 \newcommand\tooldx[1]{{\tt#1}\index{#1@{\tt#1} tool}} |
|
42 \newcommand\settdx[1]{{\tt#1}\index{#1@{\tt#1} setting}} |
|
43 |
|
44 %set argument in \tt font; at the same time, index using * prefix |
|
45 \newcommand\rmindex[1]{{#1}\index{#1}\@} |
|
46 \newcommand\ttindex[1]{{\tt#1}\index{*#1}\@} |
|
47 \newcommand\ttindexbold[1]{{\tt#1}\index{*#1|bold}\@} |
|
48 |
|
49 %set argument in \bf font and index in ROMAN font (for definitions in text!) |
|
50 \newcommand\bfindex[1]{{\bf#1}\index{#1|bold}\@} |
|
51 |
|
52 |
|
53 %%% underscores as ordinary characters, not for subscripting |
|
54 %% use @ or \sb for subscripting; use \at for @ |
|
55 %% only works in \tt font |
|
56 %% must not make _ an active char; would make \ttindex fail! |
|
57 \gdef\underscoreoff{\catcode`\@=8\catcode`\_=\other} |
|
58 \gdef\underscoreon{\catcode`\_=8\makeatother} |
|
59 \chardef\other=12 |
|
60 \chardef\at=`\@ |
|
61 |
|
62 % alternative underscore |
|
63 \def\_{\leavevmode\kern.06em\vbox{\hrule height.2ex width.3em}\hskip0.1em} |
|
64 |
|
65 %%% \dquotes permits usage of "..." for \hbox{...} -- also taken from under.sty |
|
66 {\catcode`\"=\active |
|
67 \gdef\dquotes{\catcode`\"=\active \let"=\@mathText}% |
|
68 \gdef\@mathText#1"{\hbox{\mathTextFont #1\/}}} |
|
69 \def\mathTextFont{\frenchspacing\tt} |
|
70 \def\dquotesoff{\catcode`\"=\other} |
|
71 |
|
72 %%%% meta-logical connectives |
|
73 |
|
74 \let\Forall=\bigwedge |
|
75 \let\Imp=\Longrightarrow |
|
76 \let\To=\Rightarrow |
|
77 \newcommand{\PROP}{\mathop{\mathrm{PROP}}} |
|
78 \newcommand{\Var}[1]{{?\!#1}} |
|
79 \newcommand{\All}[1]{\Forall#1.} %quantification |
|
80 |
|
81 %%%% ``WARNING'' environment |
|
82 \def\dbend{\vtop to 0pt{\vss\hbox{\Huge\bf!}\vss}} |
|
83 \newenvironment{warn}{\medskip\medbreak\begingroup \clubpenalty=10000 |
|
84 \small %%WAS\baselineskip=0.9\baselineskip |
|
85 \noindent \ifdim\parindent > 0pt\hangindent\parindent\else\hangindent1.5em\fi |
|
86 \hangafter=-2 |
|
87 \hbox to0pt{\hskip-\hangindent\dbend\hfill}\ignorespaces}% |
|
88 {\par\endgroup\medbreak} |
|
89 |
|
90 |
|
91 %%%% Standard logical symbols |
|
92 \let\turn=\vdash |
|
93 \let\conj=\wedge |
|
94 \let\disj=\vee |
|
95 \let\imp=\rightarrow |
|
96 \let\bimp=\leftrightarrow |
|
97 \newcommand\all[1]{\forall#1.} %quantification |
|
98 \newcommand\ex[1]{\exists#1.} |
|
99 \newcommand{\pair}[1]{\langle#1\rangle} |
|
100 |
|
101 \newcommand{\lparr}{\mathopen{(\!|}} |
|
102 \newcommand{\rparr}{\mathclose{|\!)}} |
|
103 \newcommand{\fs}{\mathpunct{,\,}} |
|
104 \newcommand{\ty}{\mathrel{::}} |
|
105 \newcommand{\asn}{\mathrel{:=}} |
|
106 \newcommand{\more}{\ldots} |
|
107 \newcommand{\record}[1]{\lparr #1 \rparr} |
|
108 \newcommand{\dtt}{\mathord.} |
|
109 |
|
110 \newcommand\lbrakk{\mathopen{[\![}} |
|
111 \newcommand\rbrakk{\mathclose{]\!]}} |
|
112 \newcommand\List[1]{\lbrakk#1\rbrakk} %was \obj |
|
113 \newcommand\vpile[1]{\begin{array}{c}#1\end{array}} |
|
114 \newenvironment{matharray}[1]{\[\begin{array}{#1}}{\end{array}\]} |
|
115 \newcommand{\Text}[1]{\mbox{#1}} |
|
116 |
|
117 \DeclareMathSymbol{\dshsym}{\mathalpha}{letters}{"2D} |
|
118 \newcommand{\dsh}{\mathit{\dshsym}} |
|
119 |
|
120 \let\int=\cap |
|
121 \let\un=\cup |
|
122 \let\inter=\bigcap |
|
123 \let\union=\bigcup |
|
124 |
|
125 \def\ML{{\sc ml}} |
|
126 \def\OBJ{{\sc obj}} |
|
127 \def\AST{{\sc ast}} |
|
128 |
|
129 %macros to change the treatment of symbols |
|
130 \def\relsemicolon{\mathcode`\;="303B} %treat ; like a relation |
|
131 \def\binperiod{\mathcode`\.="213A} %treat . like a binary operator |
|
132 \def\binvert{\mathcode`\|="226A} %treat | like a binary operator |
|
133 |
|
134 %redefinition of \sloppy and \fussy to use \emergencystretch |
|
135 \def\sloppy{\tolerance2000 \hfuzz.5pt \vfuzz.5pt \emergencystretch=15pt} |
|
136 \def\fussy{\tolerance200 \hfuzz.1pt \vfuzz.1pt \emergencystretch=0pt} |
|
137 |
|
138 %non-bf version of description |
|
139 \def\descrlabel#1{\hspace\labelsep #1} |
|
140 \def\descr{\list{}{\labelwidth\z@ \itemindent-\leftmargin\let\makelabel\descrlabel}} |
|
141 \let\enddescr\endlist |
|
142 |
|
143 % The mathcodes for the letters A, ..., Z, a, ..., z are changed to |
|
144 % generate text italic rather than math italic by default. This makes |
|
145 % multi-letter identifiers look better. The mathcode for character c |
|
146 % is set to |"7000| (variable family) + |"400| (text italic) + |c|. |
|
147 % |
|
148 \DeclareSymbolFont{italics}{\encodingdefault}{\rmdefault}{m}{it}% |
|
149 \def\@setmcodes#1#2#3{{\count0=#1 \count1=#3 |
|
150 \loop \global\mathcode\count0=\count1 \ifnum \count0<#2 |
|
151 \advance\count0 by1 \advance\count1 by1 \repeat}} |
|
152 \@setmcodes{`A}{`Z}{"7\hexnumber@\symitalics41} |
|
153 \@setmcodes{`a}{`z}{"7\hexnumber@\symitalics61} |