author | haftmann |
Tue, 30 Oct 2007 12:14:24 +0100 | |
changeset 25238 | ee73d4c33a88 |
parent 10092 | 4295180d6bab |
child 39860 | 788e902f3c59 |
permissions | -rw-r--r-- |
293 | 1 |
% iman.sty : Isabelle Manual Page Layout |
110 | 2 |
% |
293 | 3 |
\typeout{Document Style iman. Released 17 February 1994} |
110 | 4 |
|
293 | 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 |
|
110 | 9 |
|
301 | 10 |
%usage: \iflabelundefined{LABEL}{if not defined}{if defined} |
11 |
\newcommand{\iflabelundefined}[1]{\@ifundefined{r@#1}} |
|
12 |
||
13 |
||
110 | 14 |
%%%INDEXING use sedindex to process the index |
8827 | 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 | 17 |
\usepackage{makeidx} |
18 |
||
110 | 19 |
%index, putting page numbers of definitions in boldface |
6747 | 20 |
\def\bold#1{\textbf{#1}} |
293 | 21 |
\newcommand\fnote[1]{#1n} |
110 | 22 |
\newcommand\indexbold[1]{\index{#1|bold}} |
23 |
||
350 | 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}} |
|
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 | 39 |
\newcommand\thydx[1]{{\tt#1}\index{#1@{\tt#1} theory}} |
40 |
||
3187 | 41 |
\newcommand\tooldx[1]{{\tt#1}\index{#1@{\tt#1} tool}} |
3211 | 42 |
\newcommand\settdx[1]{{\tt#1}\index{#1@{\tt#1} setting}} |
3187 | 43 |
|
3100 | 44 |
%set argument in \tt font; at the same time, index using * prefix |
350 | 45 |
\newcommand\rmindex[1]{{#1}\index{#1}\@} |
110 | 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} |
|
6123 | 70 |
\def\dquotesoff{\catcode`\"=\other} |
110 | 71 |
|
72 |
%%%% meta-logical connectives |
|
73 |
||
74 |
\let\Forall=\bigwedge |
|
75 |
\let\Imp=\Longrightarrow |
|
76 |
\let\To=\Rightarrow |
|
7455 | 77 |
\newcommand{\PROP}{\mathop{\mathrm{PROP}}} |
78 |
\newcommand{\Var}[1]{{?\!#1}} |
|
79 |
\newcommand{\All}[1]{\Forall#1.} %quantification |
|
110 | 80 |
|
81 |
%%%% ``WARNING'' environment |
|
82 |
\def\dbend{\vtop to 0pt{\vss\hbox{\Huge\bf!}\vss}} |
|
83 |
\newenvironment{warn}{\medskip\medbreak\begingroup \clubpenalty=10000 |
|
293 | 84 |
\small %%WAS\baselineskip=0.9\baselineskip |
85 |
\noindent \hangindent\parindent \hangafter=-2 |
|
86 |
\hbox to0pt{\hskip-\hangindent\dbend\hfill}\ignorespaces}% |
|
87 |
{\par\endgroup\medbreak} |
|
110 | 88 |
|
89 |
||
90 |
%%%% Standard logical symbols |
|
91 |
\let\turn=\vdash |
|
92 |
\let\conj=\wedge |
|
93 |
\let\disj=\vee |
|
94 |
\let\imp=\rightarrow |
|
95 |
\let\bimp=\leftrightarrow |
|
293 | 96 |
\newcommand\all[1]{\forall#1.} %quantification |
110 | 97 |
\newcommand\ex[1]{\exists#1.} |
98 |
\newcommand{\pair}[1]{\langle#1\rangle} |
|
99 |
||
5752 | 100 |
\newcommand{\lparr}{\mathopen{(\!|}} |
101 |
\newcommand{\rparr}{\mathclose{|\!)}} |
|
102 |
\newcommand{\fs}{\mathpunct{,\,}} |
|
103 |
\newcommand{\ty}{\mathrel{::}} |
|
104 |
\newcommand{\asn}{\mathrel{:=}} |
|
105 |
\newcommand{\more}{\ldots} |
|
106 |
\newcommand{\record}[1]{\lparr #1 \rparr} |
|
5765 | 107 |
\newcommand{\dtt}{\mathord.} |
5752 | 108 |
|
110 | 109 |
\newcommand\lbrakk{\mathopen{[\![}} |
110 |
\newcommand\rbrakk{\mathclose{]\!]}} |
|
111 |
\newcommand\List[1]{\lbrakk#1\rbrakk} %was \obj |
|
112 |
\newcommand\vpile[1]{\begin{array}{c}#1\end{array}} |
|
5752 | 113 |
\newenvironment{matharray}[1]{\[\begin{array}{#1}}{\end{array}\]} |
9693 | 114 |
\newcommand{\Text}[1]{\mbox{#1}} |
110 | 115 |
|
7976 | 116 |
\DeclareMathSymbol{\dshsym}{\mathalpha}{letters}{"2D} |
117 |
\newcommand{\dsh}{\mathit{\dshsym}} |
|
118 |
||
110 | 119 |
\let\int=\cap |
120 |
\let\un=\cup |
|
121 |
\let\inter=\bigcap |
|
122 |
\let\union=\bigcup |
|
123 |
||
124 |
\def\ML{{\sc ml}} |
|
125 |
\def\OBJ{{\sc obj}} |
|
350 | 126 |
\def\AST{{\sc ast}} |
110 | 127 |
|
128 |
%macros to change the treatment of symbols |
|
129 |
\def\relsemicolon{\mathcode`\;="303B} %treat ; like a relation |
|
130 |
\def\binperiod{\mathcode`\.="213A} %treat . like a binary operator |
|
131 |
\def\binvert{\mathcode`\|="226A} %treat | like a binary operator |
|
132 |
||
133 |
%redefinition of \sloppy and \fussy to use \emergencystretch |
|
134 |
\def\sloppy{\tolerance2000 \hfuzz.5pt \vfuzz.5pt \emergencystretch=15pt} |
|
135 |
\def\fussy{\tolerance200 \hfuzz.1pt \vfuzz.1pt \emergencystretch=0pt} |
|
136 |
||
7169 | 137 |
%non-bf version of description |
138 |
\def\descrlabel#1{\hspace\labelsep #1} |
|
139 |
\def\descr{\list{}{\labelwidth\z@ \itemindent-\leftmargin\let\makelabel\descrlabel}} |
|
140 |
\let\enddescr\endlist |
|
141 |
||
110 | 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 | 144 |
% multi-letter identifiers look better. The mathcode for character c |
3096 | 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 | 147 |
\DeclareSymbolFont{italics}{\encodingdefault}{\rmdefault}{m}{it}% |
110 | 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 | 151 |
\@setmcodes{`A}{`Z}{"7\hexnumber@\symitalics41} |
152 |
\@setmcodes{`a}{`z}{"7\hexnumber@\symitalics61} |