doc-src/iman.sty
author nipkow
Tue, 23 Nov 1993 10:47:33 +0100
changeset 140 3a8c68d1d466
parent 110 a931f1b45151
child 293 63a0077dd9f2
permissions -rw-r--r--
changed itmath trickery to be compatible with NFSS (itmath.sty)
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
110
a931f1b45151 new style file
lcp
parents:
diff changeset
     1
\typeout{Isabelle Manual Page Layout}
a931f1b45151 new style file
lcp
parents:
diff changeset
     2
a931f1b45151 new style file
lcp
parents:
diff changeset
     3
% iman.sty 
a931f1b45151 new style file
lcp
parents:
diff changeset
     4
%
a931f1b45151 new style file
lcp
parents:
diff changeset
     5
\typeout{Document Style iman. Released 15 September 1992}
a931f1b45151 new style file
lcp
parents:
diff changeset
     6
a931f1b45151 new style file
lcp
parents:
diff changeset
     7
\hyphenation{Isa-belle}
a931f1b45151 new style file
lcp
parents:
diff changeset
     8
a931f1b45151 new style file
lcp
parents:
diff changeset
     9
%%%INDEXING  use sedindex to process the index
a931f1b45151 new style file
lcp
parents:
diff changeset
    10
%index, putting page numbers of definitions in boldface
a931f1b45151 new style file
lcp
parents:
diff changeset
    11
\newcommand\bold[1]{{\bf#1}}
a931f1b45151 new style file
lcp
parents:
diff changeset
    12
\newcommand\indexbold[1]{\index{#1|bold}}
a931f1b45151 new style file
lcp
parents:
diff changeset
    13
a931f1b45151 new style file
lcp
parents:
diff changeset
    14
%for cross-references: 2nd argument (page number) is ignored
a931f1b45151 new style file
lcp
parents:
diff changeset
    15
\newcommand\see[2]{{\it see \/}{#1}}
a931f1b45151 new style file
lcp
parents:
diff changeset
    16
\newcommand\seealso[2]{{\it see also \/}{#1}}
a931f1b45151 new style file
lcp
parents:
diff changeset
    17
a931f1b45151 new style file
lcp
parents:
diff changeset
    18
%set argument in \tt font; at the sime time, index using * prefix
a931f1b45151 new style file
lcp
parents:
diff changeset
    19
\newcommand\ttindex[1]{{\tt#1}\index{*#1}\@}
a931f1b45151 new style file
lcp
parents:
diff changeset
    20
\newcommand\ttindexbold[1]{{\tt#1}\index{*#1|bold}\@}
a931f1b45151 new style file
lcp
parents:
diff changeset
    21
a931f1b45151 new style file
lcp
parents:
diff changeset
    22
%set argument in \bf font and index in ROMAN font (for definitions in text!)
a931f1b45151 new style file
lcp
parents:
diff changeset
    23
\newcommand\bfindex[1]{{\bf#1}\index{#1|bold}\@}
a931f1b45151 new style file
lcp
parents:
diff changeset
    24
a931f1b45151 new style file
lcp
parents:
diff changeset
    25
a931f1b45151 new style file
lcp
parents:
diff changeset
    26
%%Euro-style date: 20 September 1955
a931f1b45151 new style file
lcp
parents:
diff changeset
    27
\def\today{\number\day\space\ifcase\month\or
a931f1b45151 new style file
lcp
parents:
diff changeset
    28
January\or February\or March\or April\or May\or June\or
a931f1b45151 new style file
lcp
parents:
diff changeset
    29
July\or August\or September\or October\or November\or December\fi
a931f1b45151 new style file
lcp
parents:
diff changeset
    30
\space\number\year}
a931f1b45151 new style file
lcp
parents:
diff changeset
    31
a931f1b45151 new style file
lcp
parents:
diff changeset
    32
%%% underscores as ordinary characters, not for subscripting
a931f1b45151 new style file
lcp
parents:
diff changeset
    33
%%  use @ or \sb for subscripting; use \at for @
a931f1b45151 new style file
lcp
parents:
diff changeset
    34
%%  only works in \tt font
a931f1b45151 new style file
lcp
parents:
diff changeset
    35
%%  must not make _ an active char; would make \ttindex fail!
a931f1b45151 new style file
lcp
parents:
diff changeset
    36
\gdef\underscoreoff{\catcode`\@=8\catcode`\_=\other}
a931f1b45151 new style file
lcp
parents:
diff changeset
    37
\gdef\underscoreon{\catcode`\_=8\makeatother}
a931f1b45151 new style file
lcp
parents:
diff changeset
    38
\chardef\other=12
a931f1b45151 new style file
lcp
parents:
diff changeset
    39
\chardef\at=`\@
a931f1b45151 new style file
lcp
parents:
diff changeset
    40
a931f1b45151 new style file
lcp
parents:
diff changeset
    41
% alternative underscore
a931f1b45151 new style file
lcp
parents:
diff changeset
    42
\def\_{\leavevmode\kern.06em\vbox{\hrule height.2ex width.3em}\hskip0.1em}
a931f1b45151 new style file
lcp
parents:
diff changeset
    43
a931f1b45151 new style file
lcp
parents:
diff changeset
    44
%%% \dquotes permits usage of "..." for \hbox{...} -- also taken from under.sty
a931f1b45151 new style file
lcp
parents:
diff changeset
    45
{\catcode`\"=\active
a931f1b45151 new style file
lcp
parents:
diff changeset
    46
\gdef\dquotes{\catcode`\"=\active  \let"=\@mathText}%
a931f1b45151 new style file
lcp
parents:
diff changeset
    47
\gdef\@mathText#1"{\hbox{\mathTextFont #1\/}}}
a931f1b45151 new style file
lcp
parents:
diff changeset
    48
\def\mathTextFont{\frenchspacing\tt}
a931f1b45151 new style file
lcp
parents:
diff changeset
    49
a931f1b45151 new style file
lcp
parents:
diff changeset
    50
%%%% meta-logical connectives
a931f1b45151 new style file
lcp
parents:
diff changeset
    51
a931f1b45151 new style file
lcp
parents:
diff changeset
    52
\let\Forall=\bigwedge
a931f1b45151 new style file
lcp
parents:
diff changeset
    53
\let\Imp=\Longrightarrow
a931f1b45151 new style file
lcp
parents:
diff changeset
    54
\let\To=\Rightarrow
a931f1b45151 new style file
lcp
parents:
diff changeset
    55
\newcommand\Var[1]{{?\!#1}}
a931f1b45151 new style file
lcp
parents:
diff changeset
    56
a931f1b45151 new style file
lcp
parents:
diff changeset
    57
%%%% ``WARNING'' environment
a931f1b45151 new style file
lcp
parents:
diff changeset
    58
\def\dbend{\vtop to 0pt{\vss\hbox{\Huge\bf!}\vss}}
a931f1b45151 new style file
lcp
parents:
diff changeset
    59
\newenvironment{warn}{\medskip\medbreak\begingroup \clubpenalty=10000 
a931f1b45151 new style file
lcp
parents:
diff changeset
    60
  	 \baselineskip=0.9\baselineskip
a931f1b45151 new style file
lcp
parents:
diff changeset
    61
	 \noindent \hangindent\parindent \hangafter=-2 
a931f1b45151 new style file
lcp
parents:
diff changeset
    62
  	 \hbox to0pt{\hskip-\hangindent\dbend\hfill}\ignorespaces}%
a931f1b45151 new style file
lcp
parents:
diff changeset
    63
	{\par\endgroup\medbreak}
a931f1b45151 new style file
lcp
parents:
diff changeset
    64
a931f1b45151 new style file
lcp
parents:
diff changeset
    65
a931f1b45151 new style file
lcp
parents:
diff changeset
    66
%%%% Standard logical symbols
a931f1b45151 new style file
lcp
parents:
diff changeset
    67
\let\turn=\vdash
a931f1b45151 new style file
lcp
parents:
diff changeset
    68
\let\conj=\wedge
a931f1b45151 new style file
lcp
parents:
diff changeset
    69
\let\disj=\vee
a931f1b45151 new style file
lcp
parents:
diff changeset
    70
\let\imp=\rightarrow
a931f1b45151 new style file
lcp
parents:
diff changeset
    71
\let\bimp=\leftrightarrow
a931f1b45151 new style file
lcp
parents:
diff changeset
    72
\newcommand\all[1]{\forall#1.}	%quantification
a931f1b45151 new style file
lcp
parents:
diff changeset
    73
\newcommand\ex[1]{\exists#1.}
a931f1b45151 new style file
lcp
parents:
diff changeset
    74
\newcommand{\pair}[1]{\langle#1\rangle}
a931f1b45151 new style file
lcp
parents:
diff changeset
    75
a931f1b45151 new style file
lcp
parents:
diff changeset
    76
\newenvironment{example}{\begin{Example}\rm}{\end{Example}}
a931f1b45151 new style file
lcp
parents:
diff changeset
    77
\newtheorem{Example}{Example}[chapter]
a931f1b45151 new style file
lcp
parents:
diff changeset
    78
a931f1b45151 new style file
lcp
parents:
diff changeset
    79
\newcommand\lbrakk{\mathopen{[\![}}
a931f1b45151 new style file
lcp
parents:
diff changeset
    80
\newcommand\rbrakk{\mathclose{]\!]}}
a931f1b45151 new style file
lcp
parents:
diff changeset
    81
\newcommand\List[1]{\lbrakk#1\rbrakk}  %was \obj
a931f1b45151 new style file
lcp
parents:
diff changeset
    82
\newcommand\vpile[1]{\begin{array}{c}#1\end{array}}
a931f1b45151 new style file
lcp
parents:
diff changeset
    83
a931f1b45151 new style file
lcp
parents:
diff changeset
    84
\let\int=\cap
a931f1b45151 new style file
lcp
parents:
diff changeset
    85
\let\un=\cup
a931f1b45151 new style file
lcp
parents:
diff changeset
    86
\let\inter=\bigcap
a931f1b45151 new style file
lcp
parents:
diff changeset
    87
\let\union=\bigcup
a931f1b45151 new style file
lcp
parents:
diff changeset
    88
a931f1b45151 new style file
lcp
parents:
diff changeset
    89
\newcommand{\rew}{\mathop{\longrightarrow}}
a931f1b45151 new style file
lcp
parents:
diff changeset
    90
\newcommand{\rewer}{\mathop{\longleftrightarrow}}
a931f1b45151 new style file
lcp
parents:
diff changeset
    91
a931f1b45151 new style file
lcp
parents:
diff changeset
    92
\def\ML{{\sc ml}}
a931f1b45151 new style file
lcp
parents:
diff changeset
    93
\def\OBJ{{\sc obj}}
a931f1b45151 new style file
lcp
parents:
diff changeset
    94
a931f1b45151 new style file
lcp
parents:
diff changeset
    95
\def\LCF{{\tt LCF}\@}
a931f1b45151 new style file
lcp
parents:
diff changeset
    96
\def\FOL{{\tt FOL}\@}
a931f1b45151 new style file
lcp
parents:
diff changeset
    97
\def\HOL{{\tt HOL}\@}
a931f1b45151 new style file
lcp
parents:
diff changeset
    98
\def\LK{{\tt LK}\@}
a931f1b45151 new style file
lcp
parents:
diff changeset
    99
\def\ZF{{\tt ZF}\@}
a931f1b45151 new style file
lcp
parents:
diff changeset
   100
\def\CTT{{\tt CTT}\@}
a931f1b45151 new style file
lcp
parents:
diff changeset
   101
\def\Cube{{\tt Cube}}
a931f1b45151 new style file
lcp
parents:
diff changeset
   102
\def\Modal{{\tt Modal}}
a931f1b45151 new style file
lcp
parents:
diff changeset
   103
a931f1b45151 new style file
lcp
parents:
diff changeset
   104
%macros to change the treatment of symbols
a931f1b45151 new style file
lcp
parents:
diff changeset
   105
\def\relsemicolon{\mathcode`\;="303B}   %treat ; like a relation
a931f1b45151 new style file
lcp
parents:
diff changeset
   106
\def\binperiod{\mathcode`\.="213A}   %treat . like a binary operator
a931f1b45151 new style file
lcp
parents:
diff changeset
   107
\def\binvert{\mathcode`\|="226A}     %treat | like a binary operator
a931f1b45151 new style file
lcp
parents:
diff changeset
   108
a931f1b45151 new style file
lcp
parents:
diff changeset
   109
%redefinition of \sloppy and \fussy to use \emergencystretch
a931f1b45151 new style file
lcp
parents:
diff changeset
   110
\def\sloppy{\tolerance2000 \hfuzz.5pt \vfuzz.5pt \emergencystretch=15pt}
a931f1b45151 new style file
lcp
parents:
diff changeset
   111
\def\fussy{\tolerance200 \hfuzz.1pt \vfuzz.1pt \emergencystretch=0pt}
a931f1b45151 new style file
lcp
parents:
diff changeset
   112
a931f1b45151 new style file
lcp
parents:
diff changeset
   113
\chardef\ttilde=`\~  	% A tilde for \tt font
a931f1b45151 new style file
lcp
parents:
diff changeset
   114
\chardef\ttback=`\\  	% A backslash for \tt font
a931f1b45151 new style file
lcp
parents:
diff changeset
   115
\chardef\ttlbrace=`\{ 	% A left brace for \tt font
a931f1b45151 new style file
lcp
parents:
diff changeset
   116
\chardef\ttrbrace=`\} 	% A right brace for \tt font
a931f1b45151 new style file
lcp
parents:
diff changeset
   117
a931f1b45151 new style file
lcp
parents:
diff changeset
   118
\newfont{\sltt}{cmsltt10}     %% for output from terminal sessions
a931f1b45151 new style file
lcp
parents:
diff changeset
   119
\newcommand\out{\ \sltt}
a931f1b45151 new style file
lcp
parents:
diff changeset
   120
a931f1b45151 new style file
lcp
parents:
diff changeset
   121
%Indented, boxed alltt environment; uses \small\tt font
a931f1b45151 new style file
lcp
parents:
diff changeset
   122
%\leftmargini is LaTeX's first-level indentation for items (2.5em)
a931f1b45151 new style file
lcp
parents:
diff changeset
   123
%@endparenv is LaTeX's trick for preventing indentation of next paragraph
a931f1b45151 new style file
lcp
parents:
diff changeset
   124
\newenvironment{ttbox}{\par\nobreak\vskip-2pt
a931f1b45151 new style file
lcp
parents:
diff changeset
   125
	   \vbox\bgroup \small\begin{alltt} \leftskip\leftmargini}%
a931f1b45151 new style file
lcp
parents:
diff changeset
   126
	{\end{alltt}\egroup\vskip-7pt\@endparenv}
a931f1b45151 new style file
lcp
parents:
diff changeset
   127
\newcommand\ttbreak{\end{ttbox}\vskip-10pt\begin{ttbox}}
a931f1b45151 new style file
lcp
parents:
diff changeset
   128
a931f1b45151 new style file
lcp
parents:
diff changeset
   129
a931f1b45151 new style file
lcp
parents:
diff changeset
   130
%%%Put first chapter on odd page, with arabic numbering; like \cleardoublepage
a931f1b45151 new style file
lcp
parents:
diff changeset
   131
\newcommand\clearfirst{\clearpage\ifodd\c@page\else
a931f1b45151 new style file
lcp
parents:
diff changeset
   132
    \hbox{}\newpage\if@twocolumn\hbox{}\newpage\fi\fi
a931f1b45151 new style file
lcp
parents:
diff changeset
   133
    \pagenumbering{arabic}}
a931f1b45151 new style file
lcp
parents:
diff changeset
   134
a931f1b45151 new style file
lcp
parents:
diff changeset
   135
%%%Ruled chapter headings 
a931f1b45151 new style file
lcp
parents:
diff changeset
   136
\def\@rulehead#1{\hrule height1pt \vskip 14pt \Huge \bf 
a931f1b45151 new style file
lcp
parents:
diff changeset
   137
   #1 \vskip 14pt\hrule height1pt}
a931f1b45151 new style file
lcp
parents:
diff changeset
   138
\def\@makechapterhead#1{ { \parindent 0pt 
a931f1b45151 new style file
lcp
parents:
diff changeset
   139
 \ifnum\c@secnumdepth >\m@ne \raggedleft\large\bf\@chapapp{} \thechapter \par 
a931f1b45151 new style file
lcp
parents:
diff changeset
   140
 \vskip 20pt \fi \raggedright \@rulehead{#1} \par \nobreak \vskip 40pt } }
a931f1b45151 new style file
lcp
parents:
diff changeset
   141
a931f1b45151 new style file
lcp
parents:
diff changeset
   142
\def\@makeschapterhead#1{ { \parindent 0pt \raggedright 
a931f1b45151 new style file
lcp
parents:
diff changeset
   143
 \@rulehead{#1} \par \nobreak \vskip 40pt } }
a931f1b45151 new style file
lcp
parents:
diff changeset
   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
a931f1b45151 new style file
lcp
parents:
diff changeset
   152
%
a931f1b45151 new style file
lcp
parents:
diff changeset
   153
% MATHCODES
a931f1b45151 new style file
lcp
parents:
diff changeset
   154
%
a931f1b45151 new style file
lcp
parents:
diff changeset
   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
a931f1b45151 new style file
lcp
parents:
diff changeset
   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
a931f1b45151 new style file
lcp
parents:
diff changeset
   170
a931f1b45151 new style file
lcp
parents:
diff changeset
   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
a931f1b45151 new style file
lcp
parents:
diff changeset
   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