1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/doc-src/iman.sty	Thu Nov 11 12:44:43 1993 +0100
     1.3 @@ -0,0 +1,159 @@
     1.4 +\typeout{Isabelle Manual Page Layout}
     1.5 +
     1.6 +% iman.sty 
     1.7 +%
     1.8 +\typeout{Document Style iman. Released 15 September 1992}
     1.9 +
    1.10 +\hyphenation{Isa-belle}
    1.11 +
    1.12 +%%%INDEXING  use sedindex to process the index
    1.13 +%index, putting page numbers of definitions in boldface
    1.14 +\newcommand\bold[1]{{\bf#1}}
    1.15 +\newcommand\indexbold[1]{\index{#1|bold}}
    1.16 +
    1.17 +%for cross-references: 2nd argument (page number) is ignored
    1.18 +\newcommand\see[2]{{\it see \/}{#1}}
    1.19 +\newcommand\seealso[2]{{\it see also \/}{#1}}
    1.20 +
    1.21 +%set argument in \tt font; at the sime time, index using * prefix
    1.22 +\newcommand\ttindex[1]{{\tt#1}\index{*#1}\@}
    1.23 +\newcommand\ttindexbold[1]{{\tt#1}\index{*#1|bold}\@}
    1.24 +
    1.25 +%set argument in \bf font and index in ROMAN font (for definitions in text!)
    1.26 +\newcommand\bfindex[1]{{\bf#1}\index{#1|bold}\@}
    1.27 +
    1.28 +
    1.29 +%%Euro-style date: 20 September 1955
    1.30 +\def\today{\number\day\space\ifcase\month\or
    1.31 +January\or February\or March\or April\or May\or June\or
    1.32 +July\or August\or September\or October\or November\or December\fi
    1.33 +\space\number\year}
    1.34 +
    1.35 +%%% underscores as ordinary characters, not for subscripting
    1.36 +%%  use @ or \sb for subscripting; use \at for @
    1.37 +%%  only works in \tt font
    1.38 +%%  must not make _ an active char; would make \ttindex fail!
    1.39 +\gdef\underscoreoff{\catcode`\@=8\catcode`\_=\other}
    1.40 +\gdef\underscoreon{\catcode`\_=8\makeatother}
    1.41 +\chardef\other=12
    1.42 +\chardef\at=`\@
    1.43 +
    1.44 +% alternative underscore
    1.45 +\def\_{\leavevmode\kern.06em\vbox{\hrule height.2ex width.3em}\hskip0.1em}
    1.46 +
    1.47 +%%% \dquotes permits usage of "..." for \hbox{...} -- also taken from under.sty
    1.48 +{\catcode`\"=\active
    1.49 +\gdef\dquotes{\catcode`\"=\active  \let"=\@mathText}%
    1.50 +\gdef\@mathText#1"{\hbox{\mathTextFont #1\/}}}
    1.51 +\def\mathTextFont{\frenchspacing\tt}
    1.52 +
    1.53 +%%%% meta-logical connectives
    1.54 +
    1.55 +\let\Forall=\bigwedge
    1.56 +\let\Imp=\Longrightarrow
    1.57 +\let\To=\Rightarrow
    1.58 +\newcommand\Var[1]{{?\!#1}}
    1.59 +
    1.60 +%%%% ``WARNING'' environment
    1.61 +\def\dbend{\vtop to 0pt{\vss\hbox{\Huge\bf!}\vss}}
    1.62 +\newenvironment{warn}{\medskip\medbreak\begingroup \clubpenalty=10000 
    1.63 +  	 \baselineskip=0.9\baselineskip
    1.64 +	 \noindent \hangindent\parindent \hangafter=-2 
    1.65 +  	 \hbox to0pt{\hskip-\hangindent\dbend\hfill}\ignorespaces}%
    1.66 +	{\par\endgroup\medbreak}
    1.67 +
    1.68 +
    1.69 +%%%% Standard logical symbols
    1.70 +\let\turn=\vdash
    1.71 +\let\conj=\wedge
    1.72 +\let\disj=\vee
    1.73 +\let\imp=\rightarrow
    1.74 +\let\bimp=\leftrightarrow
    1.75 +\newcommand\all[1]{\forall#1.}	%quantification
    1.76 +\newcommand\ex[1]{\exists#1.}
    1.77 +\newcommand{\pair}[1]{\langle#1\rangle}
    1.78 +
    1.79 +\newenvironment{example}{\begin{Example}\rm}{\end{Example}}
    1.80 +\newtheorem{Example}{Example}[chapter]
    1.81 +
    1.82 +\newcommand\lbrakk{\mathopen{[\![}}
    1.83 +\newcommand\rbrakk{\mathclose{]\!]}}
    1.84 +\newcommand\List[1]{\lbrakk#1\rbrakk}  %was \obj
    1.85 +\newcommand\vpile[1]{\begin{array}{c}#1\end{array}}
    1.86 +
    1.87 +\let\int=\cap
    1.88 +\let\un=\cup
    1.89 +\let\inter=\bigcap
    1.90 +\let\union=\bigcup
    1.91 +
    1.92 +\newcommand{\rew}{\mathop{\longrightarrow}}
    1.93 +\newcommand{\rewer}{\mathop{\longleftrightarrow}}
    1.94 +
    1.95 +\def\ML{{\sc ml}}
    1.96 +\def\OBJ{{\sc obj}}
    1.97 +
    1.98 +\def\LCF{{\tt LCF}\@}
    1.99 +\def\FOL{{\tt FOL}\@}
   1.100 +\def\HOL{{\tt HOL}\@}
   1.101 +\def\LK{{\tt LK}\@}
   1.102 +\def\ZF{{\tt ZF}\@}
   1.103 +\def\CTT{{\tt CTT}\@}
   1.104 +\def\Cube{{\tt Cube}}
   1.105 +\def\Modal{{\tt Modal}}
   1.106 +
   1.107 +%macros to change the treatment of symbols
   1.108 +\def\relsemicolon{\mathcode`\;="303B}   %treat ; like a relation
   1.109 +\def\binperiod{\mathcode`\.="213A}   %treat . like a binary operator
   1.110 +\def\binvert{\mathcode`\|="226A}     %treat | like a binary operator
   1.111 +
   1.112 +%redefinition of \sloppy and \fussy to use \emergencystretch
   1.113 +\def\sloppy{\tolerance2000 \hfuzz.5pt \vfuzz.5pt \emergencystretch=15pt}
   1.114 +\def\fussy{\tolerance200 \hfuzz.1pt \vfuzz.1pt \emergencystretch=0pt}
   1.115 +
   1.116 +\chardef\ttilde=`\~  	% A tilde for \tt font
   1.117 +\chardef\ttback=`\\  	% A backslash for \tt font
   1.118 +\chardef\ttlbrace=`\{ 	% A left brace for \tt font
   1.119 +\chardef\ttrbrace=`\} 	% A right brace for \tt font
   1.120 +
   1.121 +\newfont{\sltt}{cmsltt10}     %% for output from terminal sessions
   1.122 +\newcommand\out{\ \sltt}
   1.123 +
   1.124 +%Indented, boxed alltt environment; uses \small\tt font
   1.125 +%\leftmargini is LaTeX's first-level indentation for items (2.5em)
   1.126 +%@endparenv is LaTeX's trick for preventing indentation of next paragraph
   1.127 +\newenvironment{ttbox}{\par\nobreak\vskip-2pt
   1.128 +	   \vbox\bgroup \small\begin{alltt} \leftskip\leftmargini}%
   1.129 +	{\end{alltt}\egroup\vskip-7pt\@endparenv}
   1.130 +\newcommand\ttbreak{\end{ttbox}\vskip-10pt\begin{ttbox}}
   1.131 +
   1.132 +
   1.133 +%%%Put first chapter on odd page, with arabic numbering; like \cleardoublepage
   1.134 +\newcommand\clearfirst{\clearpage\ifodd\c@page\else
   1.135 +    \hbox{}\newpage\if@twocolumn\hbox{}\newpage\fi\fi
   1.136 +    \pagenumbering{arabic}}
   1.137 +
   1.138 +%%%Ruled chapter headings 
   1.139 +\def\@rulehead#1{\hrule height1pt \vskip 14pt \Huge \bf 
   1.140 +   #1 \vskip 14pt\hrule height1pt}
   1.141 +\def\@makechapterhead#1{ { \parindent 0pt 
   1.142 + \ifnum\c@secnumdepth >\m@ne \raggedleft\large\bf\@chapapp{} \thechapter \par 
   1.143 + \vskip 20pt \fi \raggedright \@rulehead{#1} \par \nobreak \vskip 40pt } }
   1.144 +
   1.145 +\def\@makeschapterhead#1{ { \parindent 0pt \raggedright 
   1.146 + \@rulehead{#1} \par \nobreak \vskip 40pt } }
   1.147 +
   1.148 +%
   1.149 +% MATHCODES
   1.150 +%
   1.151 +% The mathcodes for the letters A, ..., Z, a, ..., z are changed to
   1.152 +% generate text italic font rather than math italic by default. This makes
   1.153 +% multi-letter identifiers look better. The mathcode for character c
   1.154 +% is set to "7000 (variable family) + "400 (text italic) + c.
   1.155 +% See the TeXBook, page 154.
   1.156 +
   1.157 +\def\@setmcodes#1#2#3{{\count0=#1 \count1=#3
   1.158 +	\loop \global\mathcode\count0=\count1 \ifnum \count0<#2
   1.159 +	\advance\count0 by1 \advance\count1 by1 \repeat}}
   1.160 +
   1.161 +\@setmcodes{`A}{`Z}{"7441}
   1.162 +\@setmcodes{`a}{`z}{"7461}