doc-src/iman.sty
changeset 293 63a0077dd9f2
parent 140 3a8c68d1d466
child 301 f5ccfc4d362f
     1.1 --- a/doc-src/iman.sty	Wed Mar 23 11:32:21 1994 +0100
     1.2 +++ b/doc-src/iman.sty	Wed Mar 23 13:05:12 1994 +0100
     1.3 @@ -1,14 +1,16 @@
     1.4 -\typeout{Isabelle Manual Page Layout}
     1.5 -
     1.6 -% iman.sty 
     1.7 +% iman.sty : Isabelle Manual Page Layout
     1.8  %
     1.9 -\typeout{Document Style iman. Released 15 September 1992}
    1.10 +\typeout{Document Style iman. Released 17 February 1994}
    1.11  
    1.12 -\hyphenation{Isa-belle}
    1.13 +\hyphenation{Isa-belle man-u-script man-u-scripts ap-pen-dix mut-u-al-ly}
    1.14 +\hyphenation{data-type data-types co-data-type co-data-types }
    1.15 +
    1.16 +\let\ts=\thinspace
    1.17  
    1.18  %%%INDEXING  use sedindex to process the index
    1.19  %index, putting page numbers of definitions in boldface
    1.20  \newcommand\bold[1]{{\bf#1}}
    1.21 +\newcommand\fnote[1]{#1n}
    1.22  \newcommand\indexbold[1]{\index{#1|bold}}
    1.23  
    1.24  %for cross-references: 2nd argument (page number) is ignored
    1.25 @@ -23,12 +25,6 @@
    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 @@ -57,10 +53,10 @@
    1.39  %%%% ``WARNING'' environment
    1.40  \def\dbend{\vtop to 0pt{\vss\hbox{\Huge\bf!}\vss}}
    1.41  \newenvironment{warn}{\medskip\medbreak\begingroup \clubpenalty=10000 
    1.42 -  	 \baselineskip=0.9\baselineskip
    1.43 -	 \noindent \hangindent\parindent \hangafter=-2 
    1.44 -  	 \hbox to0pt{\hskip-\hangindent\dbend\hfill}\ignorespaces}%
    1.45 -	{\par\endgroup\medbreak}
    1.46 +         \small %%WAS\baselineskip=0.9\baselineskip
    1.47 +         \noindent \hangindent\parindent \hangafter=-2 
    1.48 +         \hbox to0pt{\hskip-\hangindent\dbend\hfill}\ignorespaces}%
    1.49 +        {\par\endgroup\medbreak}
    1.50  
    1.51  
    1.52  %%%% Standard logical symbols
    1.53 @@ -69,13 +65,10 @@
    1.54  \let\disj=\vee
    1.55  \let\imp=\rightarrow
    1.56  \let\bimp=\leftrightarrow
    1.57 -\newcommand\all[1]{\forall#1.}	%quantification
    1.58 +\newcommand\all[1]{\forall#1.}  %quantification
    1.59  \newcommand\ex[1]{\exists#1.}
    1.60  \newcommand{\pair}[1]{\langle#1\rangle}
    1.61  
    1.62 -\newenvironment{example}{\begin{Example}\rm}{\end{Example}}
    1.63 -\newtheorem{Example}{Example}[chapter]
    1.64 -
    1.65  \newcommand\lbrakk{\mathopen{[\![}}
    1.66  \newcommand\rbrakk{\mathclose{]\!]}}
    1.67  \newcommand\List[1]{\lbrakk#1\rbrakk}  %was \obj
    1.68 @@ -86,9 +79,6 @@
    1.69  \let\inter=\bigcap
    1.70  \let\union=\bigcup
    1.71  
    1.72 -\newcommand{\rew}{\mathop{\longrightarrow}}
    1.73 -\newcommand{\rewer}{\mathop{\longleftrightarrow}}
    1.74 -
    1.75  \def\ML{{\sc ml}}
    1.76  \def\OBJ{{\sc obj}}
    1.77  
    1.78 @@ -110,40 +100,16 @@
    1.79  \def\sloppy{\tolerance2000 \hfuzz.5pt \vfuzz.5pt \emergencystretch=15pt}
    1.80  \def\fussy{\tolerance200 \hfuzz.1pt \vfuzz.1pt \emergencystretch=0pt}
    1.81  
    1.82 -\chardef\ttilde=`\~  	% A tilde for \tt font
    1.83 -\chardef\ttback=`\\  	% A backslash for \tt font
    1.84 -\chardef\ttlbrace=`\{ 	% A left brace for \tt font
    1.85 -\chardef\ttrbrace=`\} 	% A right brace for \tt font
    1.86 +\chardef\ttilde=`\~     % A tilde for \tt font
    1.87 +\chardef\ttback=`\\     % A backslash for \tt font
    1.88 +\chardef\ttlbrace=`\{   % A left brace for \tt font
    1.89 +\chardef\ttrbrace=`\}   % A right brace for \tt font
    1.90  
    1.91  \newfont{\sltt}{cmsltt10}     %% for output from terminal sessions
    1.92  \newcommand\out{\ \sltt}
    1.93  
    1.94 -%Indented, boxed alltt environment; uses \small\tt font
    1.95 -%\leftmargini is LaTeX's first-level indentation for items (2.5em)
    1.96 -%@endparenv is LaTeX's trick for preventing indentation of next paragraph
    1.97 -\newenvironment{ttbox}{\par\nobreak\vskip-2pt
    1.98 -	   \vbox\bgroup \small\begin{alltt} \leftskip\leftmargini}%
    1.99 -	{\end{alltt}\egroup\vskip-7pt\@endparenv}
   1.100 -\newcommand\ttbreak{\end{ttbox}\vskip-10pt\begin{ttbox}}
   1.101 -
   1.102 -
   1.103 -%%%Put first chapter on odd page, with arabic numbering; like \cleardoublepage
   1.104 -\newcommand\clearfirst{\clearpage\ifodd\c@page\else
   1.105 -    \hbox{}\newpage\if@twocolumn\hbox{}\newpage\fi\fi
   1.106 -    \pagenumbering{arabic}}
   1.107 -
   1.108 -%%%Ruled chapter headings 
   1.109 -\def\@rulehead#1{\hrule height1pt \vskip 14pt \Huge \bf 
   1.110 -   #1 \vskip 14pt\hrule height1pt}
   1.111 -\def\@makechapterhead#1{ { \parindent 0pt 
   1.112 - \ifnum\c@secnumdepth >\m@ne \raggedleft\large\bf\@chapapp{} \thechapter \par 
   1.113 - \vskip 20pt \fi \raggedright \@rulehead{#1} \par \nobreak \vskip 40pt } }
   1.114 -
   1.115 -\def\@makeschapterhead#1{ { \parindent 0pt \raggedright 
   1.116 - \@rulehead{#1} \par \nobreak \vskip 40pt } }
   1.117 -
   1.118  % "itmath.sty" use cmr italic for letters in math mode and get the
   1.119 -%	       usual letter spacing of text mode.
   1.120 +%              usual letter spacing of text mode.
   1.121  %
   1.122  % Michael Lawley, April 1993
   1.123  % (lawley@cit.gu.edu.au)
   1.124 @@ -178,4 +144,4 @@
   1.125  \@setmcodes{`a}{`z}{"7\@tempa 61}
   1.126  
   1.127  \ifx\define@mathgroup\undefined\else
   1.128 -	\define@mathgroup\mv@normal{\itfam}{cmr}{m}{it}\fi
   1.129 +        \define@mathgroup\mv@normal{\itfam}{cmr}{m}{it}\fi