src/Doc/iman.sty
changeset 48985 5386df44a037
parent 39860 788e902f3c59
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/Doc/iman.sty	Tue Aug 28 18:57:32 2012 +0200
     1.3 @@ -0,0 +1,153 @@
     1.4 +% iman.sty : Isabelle Manual Page Layout
     1.5 +%
     1.6 +\typeout{Document Style iman. Released 17 February 1994}
     1.7 +
     1.8 +\hyphenation{Isa-belle man-u-script man-u-scripts ap-pen-dix mut-u-al-ly}
     1.9 +\hyphenation{data-type data-types co-data-type co-data-types }
    1.10 +
    1.11 +\let\ts=\thinspace
    1.12 +
    1.13 +%usage: \iflabelundefined{LABEL}{if not defined}{if defined}
    1.14 +\newcommand{\iflabelundefined}[1]{\@ifundefined{r@#1}}
    1.15 +
    1.16 +
    1.17 +%%%INDEXING  use sedindex to process the index
    1.18 +
    1.19 +\newcommand\seealso[2]{\emph{see also} #1}
    1.20 +\usepackage{makeidx}
    1.21 +
    1.22 +%index, putting page numbers of definitions in boldface
    1.23 +\def\bold#1{\textbf{#1}}
    1.24 +\newcommand\fnote[1]{#1n}
    1.25 +\newcommand\indexbold[1]{\index{#1|bold}}
    1.26 +
    1.27 +%for indexing constants, symbols, theorems, ...
    1.28 +\newcommand\cdx[1]{{\tt#1}\index{#1@{\tt#1} constant}}
    1.29 +\newcommand\sdx[1]{{\tt#1}\index{#1@{\tt#1} symbol}}
    1.30 +
    1.31 +\newcommand\tdx[1]{{\tt#1}\index{#1@{\tt#1} theorem}}
    1.32 +\newcommand\tdxbold[1]{{\tt#1}\index{#1@{\tt#1} theorem|bold}}
    1.33 +
    1.34 +\newcommand\mltydx[1]{{\tt#1}\index{#1@{\tt#1} ML type}}
    1.35 +\newcommand\xdx[1]{{\tt#1}\index{#1@{\tt#1} exception}}
    1.36 +
    1.37 +\newcommand\ndx[1]{{\tt#1}\index{#1@{\tt#1} nonterminal}}
    1.38 +\newcommand\ndxbold[1]{{\tt#1}\index{#1@{\tt#1} nonterminal|bold}}
    1.39 +
    1.40 +\newcommand\cldx[1]{{\tt#1}\index{#1@{\tt#1} class}}
    1.41 +\newcommand\tydx[1]{\textit{#1}\index{#1@{\textit{#1}} type}}
    1.42 +\newcommand\thydx[1]{{\tt#1}\index{#1@{\tt#1} theory}}
    1.43 +
    1.44 +\newcommand\tooldx[1]{{\tt#1}\index{#1@{\tt#1} tool}}
    1.45 +\newcommand\settdx[1]{{\tt#1}\index{#1@{\tt#1} setting}}
    1.46 +
    1.47 +%set argument in \tt font; at the same time, index using * prefix
    1.48 +\newcommand\rmindex[1]{{#1}\index{#1}\@}
    1.49 +\newcommand\ttindex[1]{{\tt#1}\index{*#1}\@}
    1.50 +\newcommand\ttindexbold[1]{{\tt#1}\index{*#1|bold}\@}
    1.51 +
    1.52 +%set argument in \bf font and index in ROMAN font (for definitions in text!)
    1.53 +\newcommand\bfindex[1]{{\bf#1}\index{#1|bold}\@}
    1.54 +
    1.55 +
    1.56 +%%% underscores as ordinary characters, not for subscripting
    1.57 +%%  use @ or \sb for subscripting; use \at for @
    1.58 +%%  only works in \tt font
    1.59 +%%  must not make _ an active char; would make \ttindex fail!
    1.60 +\gdef\underscoreoff{\catcode`\@=8\catcode`\_=\other}
    1.61 +\gdef\underscoreon{\catcode`\_=8\makeatother}
    1.62 +\chardef\other=12
    1.63 +\chardef\at=`\@
    1.64 +
    1.65 +% alternative underscore
    1.66 +\def\_{\leavevmode\kern.06em\vbox{\hrule height.2ex width.3em}\hskip0.1em}
    1.67 +
    1.68 +%%% \dquotes permits usage of "..." for \hbox{...} -- also taken from under.sty
    1.69 +{\catcode`\"=\active
    1.70 +\gdef\dquotes{\catcode`\"=\active  \let"=\@mathText}%
    1.71 +\gdef\@mathText#1"{\hbox{\mathTextFont #1\/}}}
    1.72 +\def\mathTextFont{\frenchspacing\tt}
    1.73 +\def\dquotesoff{\catcode`\"=\other}
    1.74 +
    1.75 +%%%% meta-logical connectives
    1.76 +
    1.77 +\let\Forall=\bigwedge
    1.78 +\let\Imp=\Longrightarrow
    1.79 +\let\To=\Rightarrow
    1.80 +\newcommand{\PROP}{\mathop{\mathrm{PROP}}}
    1.81 +\newcommand{\Var}[1]{{?\!#1}}
    1.82 +\newcommand{\All}[1]{\Forall#1.}  %quantification
    1.83 +
    1.84 +%%%% ``WARNING'' environment
    1.85 +\def\dbend{\vtop to 0pt{\vss\hbox{\Huge\bf!}\vss}}
    1.86 +\newenvironment{warn}{\medskip\medbreak\begingroup \clubpenalty=10000 
    1.87 +         \small %%WAS\baselineskip=0.9\baselineskip
    1.88 +         \noindent \ifdim\parindent > 0pt\hangindent\parindent\else\hangindent1.5em\fi
    1.89 +         \hangafter=-2
    1.90 +         \hbox to0pt{\hskip-\hangindent\dbend\hfill}\ignorespaces}%
    1.91 +        {\par\endgroup\medbreak}
    1.92 +
    1.93 +
    1.94 +%%%% Standard logical symbols
    1.95 +\let\turn=\vdash
    1.96 +\let\conj=\wedge
    1.97 +\let\disj=\vee
    1.98 +\let\imp=\rightarrow
    1.99 +\let\bimp=\leftrightarrow
   1.100 +\newcommand\all[1]{\forall#1.}  %quantification
   1.101 +\newcommand\ex[1]{\exists#1.}
   1.102 +\newcommand{\pair}[1]{\langle#1\rangle}
   1.103 +
   1.104 +\newcommand{\lparr}{\mathopen{(\!|}}
   1.105 +\newcommand{\rparr}{\mathclose{|\!)}}
   1.106 +\newcommand{\fs}{\mathpunct{,\,}}
   1.107 +\newcommand{\ty}{\mathrel{::}}
   1.108 +\newcommand{\asn}{\mathrel{:=}}
   1.109 +\newcommand{\more}{\ldots}
   1.110 +\newcommand{\record}[1]{\lparr #1 \rparr}
   1.111 +\newcommand{\dtt}{\mathord.}
   1.112 +
   1.113 +\newcommand\lbrakk{\mathopen{[\![}}
   1.114 +\newcommand\rbrakk{\mathclose{]\!]}}
   1.115 +\newcommand\List[1]{\lbrakk#1\rbrakk}  %was \obj
   1.116 +\newcommand\vpile[1]{\begin{array}{c}#1\end{array}}
   1.117 +\newenvironment{matharray}[1]{\[\begin{array}{#1}}{\end{array}\]}
   1.118 +\newcommand{\Text}[1]{\mbox{#1}}
   1.119 +
   1.120 +\DeclareMathSymbol{\dshsym}{\mathalpha}{letters}{"2D}
   1.121 +\newcommand{\dsh}{\mathit{\dshsym}}
   1.122 +
   1.123 +\let\int=\cap
   1.124 +\let\un=\cup
   1.125 +\let\inter=\bigcap
   1.126 +\let\union=\bigcup
   1.127 +
   1.128 +\def\ML{{\sc ml}}
   1.129 +\def\OBJ{{\sc obj}}
   1.130 +\def\AST{{\sc ast}}
   1.131 +
   1.132 +%macros to change the treatment of symbols
   1.133 +\def\relsemicolon{\mathcode`\;="303B}   %treat ; like a relation
   1.134 +\def\binperiod{\mathcode`\.="213A}   %treat . like a binary operator
   1.135 +\def\binvert{\mathcode`\|="226A}     %treat | like a binary operator
   1.136 +
   1.137 +%redefinition of \sloppy and \fussy to use \emergencystretch
   1.138 +\def\sloppy{\tolerance2000 \hfuzz.5pt \vfuzz.5pt \emergencystretch=15pt}
   1.139 +\def\fussy{\tolerance200 \hfuzz.1pt \vfuzz.1pt \emergencystretch=0pt}
   1.140 +
   1.141 +%non-bf version of description
   1.142 +\def\descrlabel#1{\hspace\labelsep #1}
   1.143 +\def\descr{\list{}{\labelwidth\z@ \itemindent-\leftmargin\let\makelabel\descrlabel}}
   1.144 +\let\enddescr\endlist
   1.145 +
   1.146 +% The mathcodes for the letters A, ..., Z, a, ..., z are changed to
   1.147 +% generate text italic rather than math italic by default. This makes
   1.148 +% multi-letter identifiers look better. The mathcode for character c
   1.149 +% is set to |"7000| (variable family) + |"400| (text italic) + |c|.
   1.150 +%
   1.151 +\DeclareSymbolFont{italics}{\encodingdefault}{\rmdefault}{m}{it}%
   1.152 +\def\@setmcodes#1#2#3{{\count0=#1 \count1=#3
   1.153 +        \loop \global\mathcode\count0=\count1 \ifnum \count0<#2
   1.154 +        \advance\count0 by1 \advance\count1 by1 \repeat}}
   1.155 +\@setmcodes{`A}{`Z}{"7\hexnumber@\symitalics41}
   1.156 +\@setmcodes{`a}{`z}{"7\hexnumber@\symitalics61}