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