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 +% iman.sty : Isabelle Manual Page Layout
1.6 +%
1.7 +\typeout{Document Style iman. Released 17 February 1994}
1.8
1.9 -% iman.sty
1.10 -%
1.11 -\typeout{Document Style iman. Released 15 September 1992}
1.12 +\hyphenation{Isa-belle man-u-script man-u-scripts ap-pen-dix mut-u-al-ly}
1.13 +\hyphenation{data-type data-types co-data-type co-data-types }
1.14
1.15 -\hyphenation{Isa-belle}
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