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} 154