author | lcp |
Thu, 03 Feb 1994 17:16:40 +0100 | |
changeset 263 | d45f0af592f0 |
parent 140 | 3a8c68d1d466 |
child 293 | 63a0077dd9f2 |
permissions | -rw-r--r-- |
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 |
||
140
3a8c68d1d466
changed itmath trickery to be compatible with NFSS (itmath.sty)
nipkow
parents:
110
diff
changeset
|
145 |
% "itmath.sty" use cmr italic for letters in math mode and get the |
3a8c68d1d466
changed itmath trickery to be compatible with NFSS (itmath.sty)
nipkow
parents:
110
diff
changeset
|
146 |
% usual letter spacing of text mode. |
3a8c68d1d466
changed itmath trickery to be compatible with NFSS (itmath.sty)
nipkow
parents:
110
diff
changeset
|
147 |
% |
3a8c68d1d466
changed itmath trickery to be compatible with NFSS (itmath.sty)
nipkow
parents:
110
diff
changeset
|
148 |
% Michael Lawley, April 1993 |
3a8c68d1d466
changed itmath trickery to be compatible with NFSS (itmath.sty)
nipkow
parents:
110
diff
changeset
|
149 |
% (lawley@cit.gu.edu.au) |
3a8c68d1d466
changed itmath trickery to be compatible with NFSS (itmath.sty)
nipkow
parents:
110
diff
changeset
|
150 |
% |
3a8c68d1d466
changed itmath trickery to be compatible with NFSS (itmath.sty)
nipkow
parents:
110
diff
changeset
|
151 |
% Derived from itma.sty (of unknown origin). |
110 | 152 |
% |
153 |
% MATHCODES |
|
154 |
% |
|
155 |
% 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
|
156 |
% generate text italic rather than math italic by default. This makes |
110 | 157 |
% multi-letter identifiers look better. The mathcode for character c |
140
3a8c68d1d466
changed itmath trickery to be compatible with NFSS (itmath.sty)
nipkow
parents:
110
diff
changeset
|
158 |
% is set to "7000 (variable class) + "400 (text italic) + c. |
3a8c68d1d466
changed itmath trickery to be compatible with NFSS (itmath.sty)
nipkow
parents:
110
diff
changeset
|
159 |
% |
3a8c68d1d466
changed itmath trickery to be compatible with NFSS (itmath.sty)
nipkow
parents:
110
diff
changeset
|
160 |
% For NFSS the mathcode is "7000 (variable class) + (hex)\itfam + c |
3a8c68d1d466
changed itmath trickery to be compatible with NFSS (itmath.sty)
nipkow
parents:
110
diff
changeset
|
161 |
% \itfam is probably equal to 7. |
3a8c68d1d466
changed itmath trickery to be compatible with NFSS (itmath.sty)
nipkow
parents:
110
diff
changeset
|
162 |
% |
3a8c68d1d466
changed itmath trickery to be compatible with NFSS (itmath.sty)
nipkow
parents:
110
diff
changeset
|
163 |
|
3a8c68d1d466
changed itmath trickery to be compatible with NFSS (itmath.sty)
nipkow
parents:
110
diff
changeset
|
164 |
\ifx\undefined\hexnumber@ |
3a8c68d1d466
changed itmath trickery to be compatible with NFSS (itmath.sty)
nipkow
parents:
110
diff
changeset
|
165 |
\def\hexnumber@#1{\ifcase#1 \z@ |
3a8c68d1d466
changed itmath trickery to be compatible with NFSS (itmath.sty)
nipkow
parents:
110
diff
changeset
|
166 |
\or \@ne \or \tw@ \or \thr@@ |
3a8c68d1d466
changed itmath trickery to be compatible with NFSS (itmath.sty)
nipkow
parents:
110
diff
changeset
|
167 |
\or 4\or 5\or 6\or 7\or 8\or |
3a8c68d1d466
changed itmath trickery to be compatible with NFSS (itmath.sty)
nipkow
parents:
110
diff
changeset
|
168 |
9\or A\or B\or C\or D\or E\or F\fi} |
3a8c68d1d466
changed itmath trickery to be compatible with NFSS (itmath.sty)
nipkow
parents:
110
diff
changeset
|
169 |
\fi |
110 | 170 |
|
171 |
\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
|
172 |
\loop \global\mathcode\count0=\count1 \ifnum \count0<#2 |
3a8c68d1d466
changed itmath trickery to be compatible with NFSS (itmath.sty)
nipkow
parents:
110
diff
changeset
|
173 |
\advance\count0 by1 \advance\count1 by1 \repeat}} |
3a8c68d1d466
changed itmath trickery to be compatible with NFSS (itmath.sty)
nipkow
parents:
110
diff
changeset
|
174 |
|
3a8c68d1d466
changed itmath trickery to be compatible with NFSS (itmath.sty)
nipkow
parents:
110
diff
changeset
|
175 |
\edef\@tempa{\hexnumber@\itfam} |
110 | 176 |
|
140
3a8c68d1d466
changed itmath trickery to be compatible with NFSS (itmath.sty)
nipkow
parents:
110
diff
changeset
|
177 |
\@setmcodes{`A}{`Z}{"7\@tempa 41} |
3a8c68d1d466
changed itmath trickery to be compatible with NFSS (itmath.sty)
nipkow
parents:
110
diff
changeset
|
178 |
\@setmcodes{`a}{`z}{"7\@tempa 61} |
3a8c68d1d466
changed itmath trickery to be compatible with NFSS (itmath.sty)
nipkow
parents:
110
diff
changeset
|
179 |
|
3a8c68d1d466
changed itmath trickery to be compatible with NFSS (itmath.sty)
nipkow
parents:
110
diff
changeset
|
180 |
\ifx\define@mathgroup\undefined\else |
3a8c68d1d466
changed itmath trickery to be compatible with NFSS (itmath.sty)
nipkow
parents:
110
diff
changeset
|
181 |
\define@mathgroup\mv@normal{\itfam}{cmr}{m}{it}\fi |