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