doc-src/iman.sty
changeset 9693 a2272ce2316b
parent 8829 d93e235837a9
child 10092 4295180d6bab
     1.1 --- a/doc-src/iman.sty	Mon Aug 28 13:48:25 2000 +0200
     1.2 +++ b/doc-src/iman.sty	Mon Aug 28 13:48:47 2000 +0200
     1.3 @@ -111,7 +111,7 @@
     1.4  \newcommand\List[1]{\lbrakk#1\rbrakk}  %was \obj
     1.5  \newcommand\vpile[1]{\begin{array}{c}#1\end{array}}
     1.6  \newenvironment{matharray}[1]{\[\begin{array}{#1}}{\end{array}\]}
     1.7 -\newcommand{\text}[1]{\mbox{#1}}
     1.8 +\newcommand{\Text}[1]{\mbox{#1}}
     1.9  
    1.10  \DeclareMathSymbol{\dshsym}{\mathalpha}{letters}{"2D}
    1.11  \newcommand{\dsh}{\mathit{\dshsym}}
    1.12 @@ -125,18 +125,6 @@
    1.13  \def\OBJ{{\sc obj}}
    1.14  \def\AST{{\sc ast}}
    1.15  
    1.16 -\def\Pure{{\tt Pure}\@}
    1.17 -\def\CPure{{\tt CPure}\@}
    1.18 -\def\LCF{{\tt LCF}\@}
    1.19 -\def\FOL{{\tt FOL}\@}
    1.20 -\def\HOL{{\tt HOL}\@}
    1.21 -\def\HOLCF{{\tt HOLCF}\@}
    1.22 -\def\LK{{\tt LK}\@}
    1.23 -\def\ZF{{\tt ZF}\@}
    1.24 -\def\CTT{{\tt CTT}\@}
    1.25 -\def\Cube{{\tt Cube}\@}
    1.26 -\def\Modal{{\tt Modal}\@}
    1.27 -
    1.28  %macros to change the treatment of symbols
    1.29  \def\relsemicolon{\mathcode`\;="303B}   %treat ; like a relation
    1.30  \def\binperiod{\mathcode`\.="213A}   %treat . like a binary operator
    1.31 @@ -151,21 +139,6 @@
    1.32  \def\descr{\list{}{\labelwidth\z@ \itemindent-\leftmargin\let\makelabel\descrlabel}}
    1.33  \let\enddescr\endlist
    1.34  
    1.35 -%%%% \tt things
    1.36 -
    1.37 -\def\ttdescriptionlabel#1{\hspace\labelsep \tt #1}
    1.38 -\def\ttdescription{\list{}{\labelwidth\z@ \itemindent-\leftmargin
    1.39 -       \let\makelabel\ttdescriptionlabel}}
    1.40 -
    1.41 -\let\endttdescription\endlist
    1.42 -
    1.43 -\chardef\ttilde=`\~     % A tilde for \tt font
    1.44 -\chardef\ttback=`\\     % A backslash for \tt font
    1.45 -\chardef\ttlbrace=`\{   % A left brace for \tt font
    1.46 -\chardef\ttrbrace=`\}   % A right brace for \tt font
    1.47 -
    1.48 -\newcommand\out{\ \ttfamily\slshape}   %% for output from terminal sessions
    1.49 -
    1.50  % The mathcodes for the letters A, ..., Z, a, ..., z are changed to
    1.51  % generate text italic rather than math italic by default. This makes
    1.52  % multi-letter identifiers look better. The mathcode for character c