|
1 \typeout{Isabelle Manual Page Layout} |
|
2 |
|
3 % iman.sty |
|
4 % |
|
5 \typeout{Document Style iman. Released 15 September 1992} |
|
6 |
|
7 \hyphenation{Isa-belle} |
|
8 |
|
9 %%%INDEXING use sedindex to process the index |
|
10 %index, putting page numbers of definitions in boldface |
|
11 \newcommand\bold[1]{{\bf#1}} |
|
12 \newcommand\indexbold[1]{\index{#1|bold}} |
|
13 |
|
14 %for cross-references: 2nd argument (page number) is ignored |
|
15 \newcommand\see[2]{{\it see \/}{#1}} |
|
16 \newcommand\seealso[2]{{\it see also \/}{#1}} |
|
17 |
|
18 %set argument in \tt font; at the sime time, index using * prefix |
|
19 \newcommand\ttindex[1]{{\tt#1}\index{*#1}\@} |
|
20 \newcommand\ttindexbold[1]{{\tt#1}\index{*#1|bold}\@} |
|
21 |
|
22 %set argument in \bf font and index in ROMAN font (for definitions in text!) |
|
23 \newcommand\bfindex[1]{{\bf#1}\index{#1|bold}\@} |
|
24 |
|
25 |
|
26 %%Euro-style date: 20 September 1955 |
|
27 \def\today{\number\day\space\ifcase\month\or |
|
28 January\or February\or March\or April\or May\or June\or |
|
29 July\or August\or September\or October\or November\or December\fi |
|
30 \space\number\year} |
|
31 |
|
32 %%% underscores as ordinary characters, not for subscripting |
|
33 %% use @ or \sb for subscripting; use \at for @ |
|
34 %% only works in \tt font |
|
35 %% must not make _ an active char; would make \ttindex fail! |
|
36 \gdef\underscoreoff{\catcode`\@=8\catcode`\_=\other} |
|
37 \gdef\underscoreon{\catcode`\_=8\makeatother} |
|
38 \chardef\other=12 |
|
39 \chardef\at=`\@ |
|
40 |
|
41 % alternative underscore |
|
42 \def\_{\leavevmode\kern.06em\vbox{\hrule height.2ex width.3em}\hskip0.1em} |
|
43 |
|
44 %%% \dquotes permits usage of "..." for \hbox{...} -- also taken from under.sty |
|
45 {\catcode`\"=\active |
|
46 \gdef\dquotes{\catcode`\"=\active \let"=\@mathText}% |
|
47 \gdef\@mathText#1"{\hbox{\mathTextFont #1\/}}} |
|
48 \def\mathTextFont{\frenchspacing\tt} |
|
49 |
|
50 %%%% meta-logical connectives |
|
51 |
|
52 \let\Forall=\bigwedge |
|
53 \let\Imp=\Longrightarrow |
|
54 \let\To=\Rightarrow |
|
55 \newcommand\Var[1]{{?\!#1}} |
|
56 |
|
57 %%%% ``WARNING'' environment |
|
58 \def\dbend{\vtop to 0pt{\vss\hbox{\Huge\bf!}\vss}} |
|
59 \newenvironment{warn}{\medskip\medbreak\begingroup \clubpenalty=10000 |
|
60 \baselineskip=0.9\baselineskip |
|
61 \noindent \hangindent\parindent \hangafter=-2 |
|
62 \hbox to0pt{\hskip-\hangindent\dbend\hfill}\ignorespaces}% |
|
63 {\par\endgroup\medbreak} |
|
64 |
|
65 |
|
66 %%%% Standard logical symbols |
|
67 \let\turn=\vdash |
|
68 \let\conj=\wedge |
|
69 \let\disj=\vee |
|
70 \let\imp=\rightarrow |
|
71 \let\bimp=\leftrightarrow |
|
72 \newcommand\all[1]{\forall#1.} %quantification |
|
73 \newcommand\ex[1]{\exists#1.} |
|
74 \newcommand{\pair}[1]{\langle#1\rangle} |
|
75 |
|
76 \newenvironment{example}{\begin{Example}\rm}{\end{Example}} |
|
77 \newtheorem{Example}{Example}[chapter] |
|
78 |
|
79 \newcommand\lbrakk{\mathopen{[\![}} |
|
80 \newcommand\rbrakk{\mathclose{]\!]}} |
|
81 \newcommand\List[1]{\lbrakk#1\rbrakk} %was \obj |
|
82 \newcommand\vpile[1]{\begin{array}{c}#1\end{array}} |
|
83 |
|
84 \let\int=\cap |
|
85 \let\un=\cup |
|
86 \let\inter=\bigcap |
|
87 \let\union=\bigcup |
|
88 |
|
89 \newcommand{\rew}{\mathop{\longrightarrow}} |
|
90 \newcommand{\rewer}{\mathop{\longleftrightarrow}} |
|
91 |
|
92 \def\ML{{\sc ml}} |
|
93 \def\OBJ{{\sc obj}} |
|
94 |
|
95 \def\LCF{{\tt LCF}\@} |
|
96 \def\FOL{{\tt FOL}\@} |
|
97 \def\HOL{{\tt HOL}\@} |
|
98 \def\LK{{\tt LK}\@} |
|
99 \def\ZF{{\tt ZF}\@} |
|
100 \def\CTT{{\tt CTT}\@} |
|
101 \def\Cube{{\tt Cube}} |
|
102 \def\Modal{{\tt Modal}} |
|
103 |
|
104 %macros to change the treatment of symbols |
|
105 \def\relsemicolon{\mathcode`\;="303B} %treat ; like a relation |
|
106 \def\binperiod{\mathcode`\.="213A} %treat . like a binary operator |
|
107 \def\binvert{\mathcode`\|="226A} %treat | like a binary operator |
|
108 |
|
109 %redefinition of \sloppy and \fussy to use \emergencystretch |
|
110 \def\sloppy{\tolerance2000 \hfuzz.5pt \vfuzz.5pt \emergencystretch=15pt} |
|
111 \def\fussy{\tolerance200 \hfuzz.1pt \vfuzz.1pt \emergencystretch=0pt} |
|
112 |
|
113 \chardef\ttilde=`\~ % A tilde for \tt font |
|
114 \chardef\ttback=`\\ % A backslash for \tt font |
|
115 \chardef\ttlbrace=`\{ % A left brace for \tt font |
|
116 \chardef\ttrbrace=`\} % A right brace for \tt font |
|
117 |
|
118 \newfont{\sltt}{cmsltt10} %% for output from terminal sessions |
|
119 \newcommand\out{\ \sltt} |
|
120 |
|
121 %Indented, boxed alltt environment; uses \small\tt font |
|
122 %\leftmargini is LaTeX's first-level indentation for items (2.5em) |
|
123 %@endparenv is LaTeX's trick for preventing indentation of next paragraph |
|
124 \newenvironment{ttbox}{\par\nobreak\vskip-2pt |
|
125 \vbox\bgroup \small\begin{alltt} \leftskip\leftmargini}% |
|
126 {\end{alltt}\egroup\vskip-7pt\@endparenv} |
|
127 \newcommand\ttbreak{\end{ttbox}\vskip-10pt\begin{ttbox}} |
|
128 |
|
129 |
|
130 %%%Put first chapter on odd page, with arabic numbering; like \cleardoublepage |
|
131 \newcommand\clearfirst{\clearpage\ifodd\c@page\else |
|
132 \hbox{}\newpage\if@twocolumn\hbox{}\newpage\fi\fi |
|
133 \pagenumbering{arabic}} |
|
134 |
|
135 %%%Ruled chapter headings |
|
136 \def\@rulehead#1{\hrule height1pt \vskip 14pt \Huge \bf |
|
137 #1 \vskip 14pt\hrule height1pt} |
|
138 \def\@makechapterhead#1{ { \parindent 0pt |
|
139 \ifnum\c@secnumdepth >\m@ne \raggedleft\large\bf\@chapapp{} \thechapter \par |
|
140 \vskip 20pt \fi \raggedright \@rulehead{#1} \par \nobreak \vskip 40pt } } |
|
141 |
|
142 \def\@makeschapterhead#1{ { \parindent 0pt \raggedright |
|
143 \@rulehead{#1} \par \nobreak \vskip 40pt } } |
|
144 |
|
145 % |
|
146 % MATHCODES |
|
147 % |
|
148 % The mathcodes for the letters A, ..., Z, a, ..., z are changed to |
|
149 % generate text italic font rather than math italic by default. This makes |
|
150 % multi-letter identifiers look better. The mathcode for character c |
|
151 % is set to "7000 (variable family) + "400 (text italic) + c. |
|
152 % See the TeXBook, page 154. |
|
153 |
|
154 \def\@setmcodes#1#2#3{{\count0=#1 \count1=#3 |
|
155 \loop \global\mathcode\count0=\count1 \ifnum \count0<#2 |
|
156 \advance\count0 by1 \advance\count1 by1 \repeat}} |
|
157 |
|
158 \@setmcodes{`A}{`Z}{"7441} |
|
159 \@setmcodes{`a}{`z}{"7461} |