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
|
wenzelm@8827
|
15 |
|
paulson@10092
|
16 |
\newcommand\seealso[2]{\emph{see also} #1}
|
wenzelm@8827
|
17 |
\usepackage{makeidx}
|
wenzelm@8827
|
18 |
|
lcp@110
|
19 |
%index, putting page numbers of definitions in boldface
|
wenzelm@6747
|
20 |
\def\bold#1{\textbf{#1}}
|
lcp@293
|
21 |
\newcommand\fnote[1]{#1n}
|
lcp@110
|
22 |
\newcommand\indexbold[1]{\index{#1|bold}}
|
lcp@110
|
23 |
|
lcp@350
|
24 |
%for indexing constants, symbols, theorems, ...
|
lcp@350
|
25 |
\newcommand\cdx[1]{{\tt#1}\index{#1@{\tt#1} constant}}
|
lcp@350
|
26 |
\newcommand\sdx[1]{{\tt#1}\index{#1@{\tt#1} symbol}}
|
lcp@350
|
27 |
|
lcp@350
|
28 |
\newcommand\tdx[1]{{\tt#1}\index{#1@{\tt#1} theorem}}
|
lcp@350
|
29 |
\newcommand\tdxbold[1]{{\tt#1}\index{#1@{\tt#1} theorem|bold}}
|
lcp@350
|
30 |
|
lcp@350
|
31 |
\newcommand\mltydx[1]{{\tt#1}\index{#1@{\tt#1} ML type}}
|
lcp@350
|
32 |
\newcommand\xdx[1]{{\tt#1}\index{#1@{\tt#1} exception}}
|
lcp@350
|
33 |
|
lcp@350
|
34 |
\newcommand\ndx[1]{{\tt#1}\index{#1@{\tt#1} nonterminal}}
|
lcp@350
|
35 |
\newcommand\ndxbold[1]{{\tt#1}\index{#1@{\tt#1} nonterminal|bold}}
|
lcp@350
|
36 |
|
lcp@350
|
37 |
\newcommand\cldx[1]{{\tt#1}\index{#1@{\tt#1} class}}
|
paulson@3491
|
38 |
\newcommand\tydx[1]{\textit{#1}\index{#1@{\textit{#1}} type}}
|
lcp@350
|
39 |
\newcommand\thydx[1]{{\tt#1}\index{#1@{\tt#1} theory}}
|
lcp@350
|
40 |
|
wenzelm@3187
|
41 |
\newcommand\tooldx[1]{{\tt#1}\index{#1@{\tt#1} tool}}
|
wenzelm@3211
|
42 |
\newcommand\settdx[1]{{\tt#1}\index{#1@{\tt#1} setting}}
|
wenzelm@3187
|
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
|
wenzelm@40299
|
85 |
\noindent \ifdim\parindent > 0pt\hangindent\parindent\else\hangindent1.5em\fi
|
wenzelm@40299
|
86 |
\hangafter=-2
|
lcp@293
|
87 |
\hbox to0pt{\hskip-\hangindent\dbend\hfill}\ignorespaces}%
|
lcp@293
|
88 |
{\par\endgroup\medbreak}
|
lcp@110
|
89 |
|
lcp@110
|
90 |
|
lcp@110
|
91 |
%%%% Standard logical symbols
|
lcp@110
|
92 |
\let\turn=\vdash
|
lcp@110
|
93 |
\let\conj=\wedge
|
lcp@110
|
94 |
\let\disj=\vee
|
lcp@110
|
95 |
\let\imp=\rightarrow
|
lcp@110
|
96 |
\let\bimp=\leftrightarrow
|
lcp@293
|
97 |
\newcommand\all[1]{\forall#1.} %quantification
|
lcp@110
|
98 |
\newcommand\ex[1]{\exists#1.}
|
lcp@110
|
99 |
\newcommand{\pair}[1]{\langle#1\rangle}
|
lcp@110
|
100 |
|
wenzelm@5752
|
101 |
\newcommand{\lparr}{\mathopen{(\!|}}
|
wenzelm@5752
|
102 |
\newcommand{\rparr}{\mathclose{|\!)}}
|
wenzelm@5752
|
103 |
\newcommand{\fs}{\mathpunct{,\,}}
|
wenzelm@5752
|
104 |
\newcommand{\ty}{\mathrel{::}}
|
wenzelm@5752
|
105 |
\newcommand{\asn}{\mathrel{:=}}
|
wenzelm@5752
|
106 |
\newcommand{\more}{\ldots}
|
wenzelm@5752
|
107 |
\newcommand{\record}[1]{\lparr #1 \rparr}
|
wenzelm@5765
|
108 |
\newcommand{\dtt}{\mathord.}
|
wenzelm@5752
|
109 |
|
lcp@110
|
110 |
\newcommand\lbrakk{\mathopen{[\![}}
|
lcp@110
|
111 |
\newcommand\rbrakk{\mathclose{]\!]}}
|
lcp@110
|
112 |
\newcommand\List[1]{\lbrakk#1\rbrakk} %was \obj
|
lcp@110
|
113 |
\newcommand\vpile[1]{\begin{array}{c}#1\end{array}}
|
wenzelm@5752
|
114 |
\newenvironment{matharray}[1]{\[\begin{array}{#1}}{\end{array}\]}
|
wenzelm@9693
|
115 |
\newcommand{\Text}[1]{\mbox{#1}}
|
lcp@110
|
116 |
|
wenzelm@7976
|
117 |
\DeclareMathSymbol{\dshsym}{\mathalpha}{letters}{"2D}
|
wenzelm@7976
|
118 |
\newcommand{\dsh}{\mathit{\dshsym}}
|
wenzelm@7976
|
119 |
|
lcp@110
|
120 |
\let\int=\cap
|
lcp@110
|
121 |
\let\un=\cup
|
lcp@110
|
122 |
\let\inter=\bigcap
|
lcp@110
|
123 |
\let\union=\bigcup
|
lcp@110
|
124 |
|
lcp@110
|
125 |
\def\ML{{\sc ml}}
|
lcp@110
|
126 |
\def\OBJ{{\sc obj}}
|
lcp@350
|
127 |
\def\AST{{\sc ast}}
|
lcp@110
|
128 |
|
lcp@110
|
129 |
%macros to change the treatment of symbols
|
lcp@110
|
130 |
\def\relsemicolon{\mathcode`\;="303B} %treat ; like a relation
|
lcp@110
|
131 |
\def\binperiod{\mathcode`\.="213A} %treat . like a binary operator
|
lcp@110
|
132 |
\def\binvert{\mathcode`\|="226A} %treat | like a binary operator
|
lcp@110
|
133 |
|
lcp@110
|
134 |
%redefinition of \sloppy and \fussy to use \emergencystretch
|
lcp@110
|
135 |
\def\sloppy{\tolerance2000 \hfuzz.5pt \vfuzz.5pt \emergencystretch=15pt}
|
lcp@110
|
136 |
\def\fussy{\tolerance200 \hfuzz.1pt \vfuzz.1pt \emergencystretch=0pt}
|
lcp@110
|
137 |
|
wenzelm@7169
|
138 |
%non-bf version of description
|
wenzelm@7169
|
139 |
\def\descrlabel#1{\hspace\labelsep #1}
|
wenzelm@7169
|
140 |
\def\descr{\list{}{\labelwidth\z@ \itemindent-\leftmargin\let\makelabel\descrlabel}}
|
wenzelm@7169
|
141 |
\let\enddescr\endlist
|
wenzelm@7169
|
142 |
|
lcp@110
|
143 |
% The mathcodes for the letters A, ..., Z, a, ..., z are changed to
|
nipkow@140
|
144 |
% generate text italic rather than math italic by default. This makes
|
lcp@110
|
145 |
% multi-letter identifiers look better. The mathcode for character c
|
berghofe@3096
|
146 |
% is set to |"7000| (variable family) + |"400| (text italic) + |c|.
|
nipkow@140
|
147 |
%
|
berghofe@3096
|
148 |
\DeclareSymbolFont{italics}{\encodingdefault}{\rmdefault}{m}{it}%
|
lcp@110
|
149 |
\def\@setmcodes#1#2#3{{\count0=#1 \count1=#3
|
nipkow@140
|
150 |
\loop \global\mathcode\count0=\count1 \ifnum \count0<#2
|
nipkow@140
|
151 |
\advance\count0 by1 \advance\count1 by1 \repeat}}
|
berghofe@3096
|
152 |
\@setmcodes{`A}{`Z}{"7\hexnumber@\symitalics41}
|
berghofe@3096
|
153 |
\@setmcodes{`a}{`z}{"7\hexnumber@\symitalics61}
|