109 \newcommand\lbrakk{\mathopen{[\![}} |
109 \newcommand\lbrakk{\mathopen{[\![}} |
110 \newcommand\rbrakk{\mathclose{]\!]}} |
110 \newcommand\rbrakk{\mathclose{]\!]}} |
111 \newcommand\List[1]{\lbrakk#1\rbrakk} %was \obj |
111 \newcommand\List[1]{\lbrakk#1\rbrakk} %was \obj |
112 \newcommand\vpile[1]{\begin{array}{c}#1\end{array}} |
112 \newcommand\vpile[1]{\begin{array}{c}#1\end{array}} |
113 \newenvironment{matharray}[1]{\[\begin{array}{#1}}{\end{array}\]} |
113 \newenvironment{matharray}[1]{\[\begin{array}{#1}}{\end{array}\]} |
114 \newcommand{\text}[1]{\mbox{#1}} |
114 \newcommand{\Text}[1]{\mbox{#1}} |
115 |
115 |
116 \DeclareMathSymbol{\dshsym}{\mathalpha}{letters}{"2D} |
116 \DeclareMathSymbol{\dshsym}{\mathalpha}{letters}{"2D} |
117 \newcommand{\dsh}{\mathit{\dshsym}} |
117 \newcommand{\dsh}{\mathit{\dshsym}} |
118 |
118 |
119 \let\int=\cap |
119 \let\int=\cap |
122 \let\union=\bigcup |
122 \let\union=\bigcup |
123 |
123 |
124 \def\ML{{\sc ml}} |
124 \def\ML{{\sc ml}} |
125 \def\OBJ{{\sc obj}} |
125 \def\OBJ{{\sc obj}} |
126 \def\AST{{\sc ast}} |
126 \def\AST{{\sc ast}} |
127 |
|
128 \def\Pure{{\tt Pure}\@} |
|
129 \def\CPure{{\tt CPure}\@} |
|
130 \def\LCF{{\tt LCF}\@} |
|
131 \def\FOL{{\tt FOL}\@} |
|
132 \def\HOL{{\tt HOL}\@} |
|
133 \def\HOLCF{{\tt HOLCF}\@} |
|
134 \def\LK{{\tt LK}\@} |
|
135 \def\ZF{{\tt ZF}\@} |
|
136 \def\CTT{{\tt CTT}\@} |
|
137 \def\Cube{{\tt Cube}\@} |
|
138 \def\Modal{{\tt Modal}\@} |
|
139 |
127 |
140 %macros to change the treatment of symbols |
128 %macros to change the treatment of symbols |
141 \def\relsemicolon{\mathcode`\;="303B} %treat ; like a relation |
129 \def\relsemicolon{\mathcode`\;="303B} %treat ; like a relation |
142 \def\binperiod{\mathcode`\.="213A} %treat . like a binary operator |
130 \def\binperiod{\mathcode`\.="213A} %treat . like a binary operator |
143 \def\binvert{\mathcode`\|="226A} %treat | like a binary operator |
131 \def\binvert{\mathcode`\|="226A} %treat | like a binary operator |
149 %non-bf version of description |
137 %non-bf version of description |
150 \def\descrlabel#1{\hspace\labelsep #1} |
138 \def\descrlabel#1{\hspace\labelsep #1} |
151 \def\descr{\list{}{\labelwidth\z@ \itemindent-\leftmargin\let\makelabel\descrlabel}} |
139 \def\descr{\list{}{\labelwidth\z@ \itemindent-\leftmargin\let\makelabel\descrlabel}} |
152 \let\enddescr\endlist |
140 \let\enddescr\endlist |
153 |
141 |
154 %%%% \tt things |
|
155 |
|
156 \def\ttdescriptionlabel#1{\hspace\labelsep \tt #1} |
|
157 \def\ttdescription{\list{}{\labelwidth\z@ \itemindent-\leftmargin |
|
158 \let\makelabel\ttdescriptionlabel}} |
|
159 |
|
160 \let\endttdescription\endlist |
|
161 |
|
162 \chardef\ttilde=`\~ % A tilde for \tt font |
|
163 \chardef\ttback=`\\ % A backslash for \tt font |
|
164 \chardef\ttlbrace=`\{ % A left brace for \tt font |
|
165 \chardef\ttrbrace=`\} % A right brace for \tt font |
|
166 |
|
167 \newcommand\out{\ \ttfamily\slshape} %% for output from terminal sessions |
|
168 |
|
169 % The mathcodes for the letters A, ..., Z, a, ..., z are changed to |
142 % The mathcodes for the letters A, ..., Z, a, ..., z are changed to |
170 % generate text italic rather than math italic by default. This makes |
143 % generate text italic rather than math italic by default. This makes |
171 % multi-letter identifiers look better. The mathcode for character c |
144 % multi-letter identifiers look better. The mathcode for character c |
172 % is set to |"7000| (variable family) + |"400| (text italic) + |c|. |
145 % is set to |"7000| (variable family) + |"400| (text italic) + |c|. |
173 % |
146 % |