1 % iman.sty : Isabelle Manual Page Layout
3 \typeout{Document Style iman. Released 17 February 1994}
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 }
10 %usage: \iflabelundefined{LABEL}{if not defined}{if defined}
11 \newcommand{\iflabelundefined}[1]{\@ifundefined{r@#1}}
14 %%%INDEXING use sedindex to process the index
15 %index, putting page numbers of definitions in boldface
16 \newcommand\bold[1]{{\bf#1}}
17 \newcommand\fnote[1]{#1n}
18 \newcommand\indexbold[1]{\index{#1|bold}}
20 %for cross-references: 2nd argument (page number) is ignored
21 \newcommand\see[2]{{\it see \/}{#1}}
22 \newcommand\seealso[2]{{\it see also \/}{#1}}
24 %set argument in \tt font; at the sime time, index using * prefix
25 \newcommand\ttindex[1]{{\tt#1}\index{*#1}\@}
26 \newcommand\ttindexbold[1]{{\tt#1}\index{*#1|bold}\@}
28 %set argument in \bf font and index in ROMAN font (for definitions in text!)
29 \newcommand\bfindex[1]{{\bf#1}\index{#1|bold}\@}
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 \small %%WAS\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 \newcommand\lbrakk{\mathopen{[\![}}
77 \newcommand\rbrakk{\mathclose{]\!]}}
78 \newcommand\List[1]{\lbrakk#1\rbrakk} %was \obj
79 \newcommand\vpile[1]{\begin{array}{c}#1\end{array}}
96 \def\Modal{{\tt Modal}}
98 %macros to change the treatment of symbols
99 \def\relsemicolon{\mathcode`\;="303B} %treat ; like a relation
100 \def\binperiod{\mathcode`\.="213A} %treat . like a binary operator
101 \def\binvert{\mathcode`\|="226A} %treat | like a binary operator
103 %redefinition of \sloppy and \fussy to use \emergencystretch
104 \def\sloppy{\tolerance2000 \hfuzz.5pt \vfuzz.5pt \emergencystretch=15pt}
105 \def\fussy{\tolerance200 \hfuzz.1pt \vfuzz.1pt \emergencystretch=0pt}
107 \chardef\ttilde=`\~ % A tilde for \tt font
108 \chardef\ttback=`\\ % A backslash for \tt font
109 \chardef\ttlbrace=`\{ % A left brace for \tt font
110 \chardef\ttrbrace=`\} % A right brace for \tt font
112 \newfont{\sltt}{cmsltt10} %% for output from terminal sessions
113 \newcommand\out{\ \sltt}
115 % "itmath.sty" use cmr italic for letters in math mode and get the
116 % usual letter spacing of text mode.
118 % Michael Lawley, April 1993
119 % (lawley@cit.gu.edu.au)
121 % Derived from itma.sty (of unknown origin).
125 % The mathcodes for the letters A, ..., Z, a, ..., z are changed to
126 % generate text italic rather than math italic by default. This makes
127 % multi-letter identifiers look better. The mathcode for character c
128 % is set to "7000 (variable class) + "400 (text italic) + c.
130 % For NFSS the mathcode is "7000 (variable class) + (hex)\itfam + c
131 % \itfam is probably equal to 7.
134 \ifx\undefined\hexnumber@
135 \def\hexnumber@#1{\ifcase#1 \z@
136 \or \@ne \or \tw@ \or \thr@@
137 \or 4\or 5\or 6\or 7\or 8\or
138 9\or A\or B\or C\or D\or E\or F\fi}
141 \def\@setmcodes#1#2#3{{\count0=#1 \count1=#3
142 \loop \global\mathcode\count0=\count1 \ifnum \count0<#2
143 \advance\count0 by1 \advance\count1 by1 \repeat}}
145 \edef\@tempa{\hexnumber@\itfam}
147 \@setmcodes{`A}{`Z}{"7\@tempa 41}
148 \@setmcodes{`a}{`z}{"7\@tempa 61}
150 \ifx\define@mathgroup\undefined\else
151 \define@mathgroup\mv@normal{\itfam}{cmr}{m}{it}\fi