author | lcp |
Thu, 24 Mar 1994 16:12:42 +0100 | |
changeset 301 | f5ccfc4d362f |
parent 293 | 63a0077dd9f2 |
child 350 | d9ebca601847 |
permissions | -rw-r--r-- |
lcp@293 | 1 |
% iman.sty : Isabelle Manual Page Layout |
lcp@293 | 2 |
% |
lcp@293 | 3 |
\typeout{Document Style iman. Released 17 February 1994} |
lcp@110 | 4 |
|
lcp@293 | 5 |
\hyphenation{Isa-belle man-u-script man-u-scripts ap-pen-dix mut-u-al-ly} |
lcp@293 | 6 |
\hyphenation{data-type data-types co-data-type co-data-types } |
lcp@110 | 7 |
|
lcp@293 | 8 |
\let\ts=\thinspace |
lcp@110 | 9 |
|
lcp@301 | 10 |
%usage: \iflabelundefined{LABEL}{if not defined}{if defined} |
lcp@301 | 11 |
\newcommand{\iflabelundefined}[1]{\@ifundefined{r@#1}} |
lcp@301 | 12 |
|
lcp@301 | 13 |
|
lcp@110 | 14 |
%%%INDEXING use sedindex to process the index |
lcp@110 | 15 |
%index, putting page numbers of definitions in boldface |
lcp@110 | 16 |
\newcommand\bold[1]{{\bf#1}} |
lcp@293 | 17 |
\newcommand\fnote[1]{#1n} |
lcp@110 | 18 |
\newcommand\indexbold[1]{\index{#1|bold}} |
lcp@110 | 19 |
|
lcp@110 | 20 |
%for cross-references: 2nd argument (page number) is ignored |
lcp@110 | 21 |
\newcommand\see[2]{{\it see \/}{#1}} |
lcp@110 | 22 |
\newcommand\seealso[2]{{\it see also \/}{#1}} |
lcp@110 | 23 |
|
lcp@110 | 24 |
%set argument in \tt font; at the sime time, index using * prefix |
lcp@110 | 25 |
\newcommand\ttindex[1]{{\tt#1}\index{*#1}\@} |
lcp@110 | 26 |
\newcommand\ttindexbold[1]{{\tt#1}\index{*#1|bold}\@} |
lcp@110 | 27 |
|
lcp@110 | 28 |
%set argument in \bf font and index in ROMAN font (for definitions in text!) |
lcp@110 | 29 |
\newcommand\bfindex[1]{{\bf#1}\index{#1|bold}\@} |
lcp@110 | 30 |
|
lcp@110 | 31 |
|
lcp@110 | 32 |
%%% underscores as ordinary characters, not for subscripting |
lcp@110 | 33 |
%% use @ or \sb for subscripting; use \at for @ |
lcp@110 | 34 |
%% only works in \tt font |
lcp@110 | 35 |
%% must not make _ an active char; would make \ttindex fail! |
lcp@110 | 36 |
\gdef\underscoreoff{\catcode`\@=8\catcode`\_=\other} |
lcp@110 | 37 |
\gdef\underscoreon{\catcode`\_=8\makeatother} |
lcp@110 | 38 |
\chardef\other=12 |
lcp@110 | 39 |
\chardef\at=`\@ |
lcp@110 | 40 |
|
lcp@110 | 41 |
% alternative underscore |
lcp@110 | 42 |
\def\_{\leavevmode\kern.06em\vbox{\hrule height.2ex width.3em}\hskip0.1em} |
lcp@110 | 43 |
|
lcp@110 | 44 |
%%% \dquotes permits usage of "..." for \hbox{...} -- also taken from under.sty |
lcp@110 | 45 |
{\catcode`\"=\active |
lcp@110 | 46 |
\gdef\dquotes{\catcode`\"=\active \let"=\@mathText}% |
lcp@110 | 47 |
\gdef\@mathText#1"{\hbox{\mathTextFont #1\/}}} |
lcp@110 | 48 |
\def\mathTextFont{\frenchspacing\tt} |
lcp@110 | 49 |
|
lcp@110 | 50 |
%%%% meta-logical connectives |
lcp@110 | 51 |
|
lcp@110 | 52 |
\let\Forall=\bigwedge |
lcp@110 | 53 |
\let\Imp=\Longrightarrow |
lcp@110 | 54 |
\let\To=\Rightarrow |
lcp@110 | 55 |
\newcommand\Var[1]{{?\!#1}} |
lcp@110 | 56 |
|
lcp@110 | 57 |
%%%% ``WARNING'' environment |
lcp@110 | 58 |
\def\dbend{\vtop to 0pt{\vss\hbox{\Huge\bf!}\vss}} |
lcp@110 | 59 |
\newenvironment{warn}{\medskip\medbreak\begingroup \clubpenalty=10000 |
lcp@293 | 60 |
\small %%WAS\baselineskip=0.9\baselineskip |
lcp@293 | 61 |
\noindent \hangindent\parindent \hangafter=-2 |
lcp@293 | 62 |
\hbox to0pt{\hskip-\hangindent\dbend\hfill}\ignorespaces}% |
lcp@293 | 63 |
{\par\endgroup\medbreak} |
lcp@110 | 64 |
|
lcp@110 | 65 |
|
lcp@110 | 66 |
%%%% Standard logical symbols |
lcp@110 | 67 |
\let\turn=\vdash |
lcp@110 | 68 |
\let\conj=\wedge |
lcp@110 | 69 |
\let\disj=\vee |
lcp@110 | 70 |
\let\imp=\rightarrow |
lcp@110 | 71 |
\let\bimp=\leftrightarrow |
lcp@293 | 72 |
\newcommand\all[1]{\forall#1.} %quantification |
lcp@110 | 73 |
\newcommand\ex[1]{\exists#1.} |
lcp@110 | 74 |
\newcommand{\pair}[1]{\langle#1\rangle} |
lcp@110 | 75 |
|
lcp@110 | 76 |
\newcommand\lbrakk{\mathopen{[\![}} |
lcp@110 | 77 |
\newcommand\rbrakk{\mathclose{]\!]}} |
lcp@110 | 78 |
\newcommand\List[1]{\lbrakk#1\rbrakk} %was \obj |
lcp@110 | 79 |
\newcommand\vpile[1]{\begin{array}{c}#1\end{array}} |
lcp@110 | 80 |
|
lcp@110 | 81 |
\let\int=\cap |
lcp@110 | 82 |
\let\un=\cup |
lcp@110 | 83 |
\let\inter=\bigcap |
lcp@110 | 84 |
\let\union=\bigcup |
lcp@110 | 85 |
|
lcp@110 | 86 |
\def\ML{{\sc ml}} |
lcp@110 | 87 |
\def\OBJ{{\sc obj}} |
lcp@110 | 88 |
|
lcp@110 | 89 |
\def\LCF{{\tt LCF}\@} |
lcp@110 | 90 |
\def\FOL{{\tt FOL}\@} |
lcp@110 | 91 |
\def\HOL{{\tt HOL}\@} |
lcp@110 | 92 |
\def\LK{{\tt LK}\@} |
lcp@110 | 93 |
\def\ZF{{\tt ZF}\@} |
lcp@110 | 94 |
\def\CTT{{\tt CTT}\@} |
lcp@110 | 95 |
\def\Cube{{\tt Cube}} |
lcp@110 | 96 |
\def\Modal{{\tt Modal}} |
lcp@110 | 97 |
|
lcp@110 | 98 |
%macros to change the treatment of symbols |
lcp@110 | 99 |
\def\relsemicolon{\mathcode`\;="303B} %treat ; like a relation |
lcp@110 | 100 |
\def\binperiod{\mathcode`\.="213A} %treat . like a binary operator |
lcp@110 | 101 |
\def\binvert{\mathcode`\|="226A} %treat | like a binary operator |
lcp@110 | 102 |
|
lcp@110 | 103 |
%redefinition of \sloppy and \fussy to use \emergencystretch |
lcp@110 | 104 |
\def\sloppy{\tolerance2000 \hfuzz.5pt \vfuzz.5pt \emergencystretch=15pt} |
lcp@110 | 105 |
\def\fussy{\tolerance200 \hfuzz.1pt \vfuzz.1pt \emergencystretch=0pt} |
lcp@110 | 106 |
|
lcp@293 | 107 |
\chardef\ttilde=`\~ % A tilde for \tt font |
lcp@293 | 108 |
\chardef\ttback=`\\ % A backslash for \tt font |
lcp@293 | 109 |
\chardef\ttlbrace=`\{ % A left brace for \tt font |
lcp@293 | 110 |
\chardef\ttrbrace=`\} % A right brace for \tt font |
lcp@110 | 111 |
|
lcp@110 | 112 |
\newfont{\sltt}{cmsltt10} %% for output from terminal sessions |
lcp@110 | 113 |
\newcommand\out{\ \sltt} |
lcp@110 | 114 |
|
nipkow@140 | 115 |
% "itmath.sty" use cmr italic for letters in math mode and get the |
lcp@293 | 116 |
% usual letter spacing of text mode. |
nipkow@140 | 117 |
% |
nipkow@140 | 118 |
% Michael Lawley, April 1993 |
nipkow@140 | 119 |
% (lawley@cit.gu.edu.au) |
nipkow@140 | 120 |
% |
nipkow@140 | 121 |
% Derived from itma.sty (of unknown origin). |
lcp@110 | 122 |
% |
lcp@110 | 123 |
% MATHCODES |
lcp@110 | 124 |
% |
lcp@110 | 125 |
% The mathcodes for the letters A, ..., Z, a, ..., z are changed to |
nipkow@140 | 126 |
% generate text italic rather than math italic by default. This makes |
lcp@110 | 127 |
% multi-letter identifiers look better. The mathcode for character c |
nipkow@140 | 128 |
% is set to "7000 (variable class) + "400 (text italic) + c. |
nipkow@140 | 129 |
% |
nipkow@140 | 130 |
% For NFSS the mathcode is "7000 (variable class) + (hex)\itfam + c |
nipkow@140 | 131 |
% \itfam is probably equal to 7. |
nipkow@140 | 132 |
% |
nipkow@140 | 133 |
|
nipkow@140 | 134 |
\ifx\undefined\hexnumber@ |
nipkow@140 | 135 |
\def\hexnumber@#1{\ifcase#1 \z@ |
nipkow@140 | 136 |
\or \@ne \or \tw@ \or \thr@@ |
nipkow@140 | 137 |
\or 4\or 5\or 6\or 7\or 8\or |
nipkow@140 | 138 |
9\or A\or B\or C\or D\or E\or F\fi} |
nipkow@140 | 139 |
\fi |
lcp@110 | 140 |
|
lcp@110 | 141 |
\def\@setmcodes#1#2#3{{\count0=#1 \count1=#3 |
nipkow@140 | 142 |
\loop \global\mathcode\count0=\count1 \ifnum \count0<#2 |
nipkow@140 | 143 |
\advance\count0 by1 \advance\count1 by1 \repeat}} |
lcp@110 | 144 |
|
nipkow@140 | 145 |
\edef\@tempa{\hexnumber@\itfam} |
nipkow@140 | 146 |
|
nipkow@140 | 147 |
\@setmcodes{`A}{`Z}{"7\@tempa 41} |
nipkow@140 | 148 |
\@setmcodes{`a}{`z}{"7\@tempa 61} |
nipkow@140 | 149 |
|
nipkow@140 | 150 |
\ifx\define@mathgroup\undefined\else |
lcp@293 | 151 |
\define@mathgroup\mv@normal{\itfam}{cmr}{m}{it}\fi |