# HG changeset patch
# User wenzelm
# Date 967463327 -7200
# Node ID a2272ce2316bbd6afe53d4432de1003abcf82901
# Parent  e15aaebea14db2d3a0b8f1bedfbcc3896f4c6fd7
moved \tt things to ttbox.sty;
removed \Pure etc;

diff -r e15aaebea14d -r a2272ce2316b doc-src/iman.sty
--- a/doc-src/iman.sty	Mon Aug 28 13:48:25 2000 +0200
+++ b/doc-src/iman.sty	Mon Aug 28 13:48:47 2000 +0200
@@ -111,7 +111,7 @@
 \newcommand\List[1]{\lbrakk#1\rbrakk}  %was \obj
 \newcommand\vpile[1]{\begin{array}{c}#1\end{array}}
 \newenvironment{matharray}[1]{\[\begin{array}{#1}}{\end{array}\]}
-\newcommand{\text}[1]{\mbox{#1}}
+\newcommand{\Text}[1]{\mbox{#1}}
 
 \DeclareMathSymbol{\dshsym}{\mathalpha}{letters}{"2D}
 \newcommand{\dsh}{\mathit{\dshsym}}
@@ -125,18 +125,6 @@
 \def\OBJ{{\sc obj}}
 \def\AST{{\sc ast}}
 
-\def\Pure{{\tt Pure}\@}
-\def\CPure{{\tt CPure}\@}
-\def\LCF{{\tt LCF}\@}
-\def\FOL{{\tt FOL}\@}
-\def\HOL{{\tt HOL}\@}
-\def\HOLCF{{\tt HOLCF}\@}
-\def\LK{{\tt LK}\@}
-\def\ZF{{\tt ZF}\@}
-\def\CTT{{\tt CTT}\@}
-\def\Cube{{\tt Cube}\@}
-\def\Modal{{\tt Modal}\@}
-
 %macros to change the treatment of symbols
 \def\relsemicolon{\mathcode`\;="303B}   %treat ; like a relation
 \def\binperiod{\mathcode`\.="213A}   %treat . like a binary operator
@@ -151,21 +139,6 @@
 \def\descr{\list{}{\labelwidth\z@ \itemindent-\leftmargin\let\makelabel\descrlabel}}
 \let\enddescr\endlist
 
-%%%% \tt things
-
-\def\ttdescriptionlabel#1{\hspace\labelsep \tt #1}
-\def\ttdescription{\list{}{\labelwidth\z@ \itemindent-\leftmargin
-       \let\makelabel\ttdescriptionlabel}}
-
-\let\endttdescription\endlist
-
-\chardef\ttilde=`\~     % A tilde for \tt font
-\chardef\ttback=`\\     % A backslash for \tt font
-\chardef\ttlbrace=`\{   % A left brace for \tt font
-\chardef\ttrbrace=`\}   % A right brace for \tt font
-
-\newcommand\out{\ \ttfamily\slshape}   %% for output from terminal sessions
-
 % The mathcodes for the letters A, ..., Z, a, ..., z are changed to
 % generate text italic rather than math italic by default. This makes
 % multi-letter identifiers look better. The mathcode for character c