1 \typeout{Isabelle Manual Page Layout}
5 \typeout{Document Style iman. Released 15 September 1992}
7 \hyphenation{Isa-belle}
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}}
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}}
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}\@}
22 %set argument in \bf font and index in ROMAN font (for definitions in text!)
23 \newcommand\bfindex[1]{{\bf#1}\index{#1|bold}\@}
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
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}
41 % alternative underscore
42 \def\_{\leavevmode\kern.06em\vbox{\hrule height.2ex width.3em}\hskip0.1em}
44 %%% \dquotes permits usage of "..." for \hbox{...} -- also taken from under.sty
46 \gdef\dquotes{\catcode`\"=\active \let"=\@mathText}%
47 \gdef\@mathText#1"{\hbox{\mathTextFont #1\/}}}
48 \def\mathTextFont{\frenchspacing\tt}
50 %%%% meta-logical connectives
53 \let\Imp=\Longrightarrow
55 \newcommand\Var[1]{{?\!#1}}
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}
66 %%%% Standard logical symbols
71 \let\bimp=\leftrightarrow
72 \newcommand\all[1]{\forall#1.} %quantification
73 \newcommand\ex[1]{\exists#1.}
74 \newcommand{\pair}[1]{\langle#1\rangle}
76 \newenvironment{example}{\begin{Example}\rm}{\end{Example}}
77 \newtheorem{Example}{Example}[chapter]
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}}
89 \newcommand{\rew}{\mathop{\longrightarrow}}
90 \newcommand{\rewer}{\mathop{\longleftrightarrow}}
100 \def\CTT{{\tt CTT}\@}
101 \def\Cube{{\tt Cube}}
102 \def\Modal{{\tt Modal}}
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
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}
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
118 \newfont{\sltt}{cmsltt10} %% for output from terminal sessions
119 \newcommand\out{\ \sltt}
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}}
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}}
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 } }
142 \def\@makeschapterhead#1{ { \parindent 0pt \raggedright
143 \@rulehead{#1} \par \nobreak \vskip 40pt } }
145 % "itmath.sty" use cmr italic for letters in math mode and get the
146 % usual letter spacing of text mode.
148 % Michael Lawley, April 1993
149 % (lawley@cit.gu.edu.au)
151 % Derived from itma.sty (of unknown origin).
155 % The mathcodes for the letters A, ..., Z, a, ..., z are changed to
156 % generate text italic rather than math italic by default. This makes
157 % multi-letter identifiers look better. The mathcode for character c
158 % is set to "7000 (variable class) + "400 (text italic) + c.
160 % For NFSS the mathcode is "7000 (variable class) + (hex)\itfam + c
161 % \itfam is probably equal to 7.
164 \ifx\undefined\hexnumber@
165 \def\hexnumber@#1{\ifcase#1 \z@
166 \or \@ne \or \tw@ \or \thr@@
167 \or 4\or 5\or 6\or 7\or 8\or
168 9\or A\or B\or C\or D\or E\or F\fi}
171 \def\@setmcodes#1#2#3{{\count0=#1 \count1=#3
172 \loop \global\mathcode\count0=\count1 \ifnum \count0<#2
173 \advance\count0 by1 \advance\count1 by1 \repeat}}
175 \edef\@tempa{\hexnumber@\itfam}
177 \@setmcodes{`A}{`Z}{"7\@tempa 41}
178 \@setmcodes{`a}{`z}{"7\@tempa 61}
180 \ifx\define@mathgroup\undefined\else
181 \define@mathgroup\mv@normal{\itfam}{cmr}{m}{it}\fi