doc-src/iman.sty
changeset 350 d9ebca601847
parent 301 f5ccfc4d362f
child 1112 737a1a0df754
equal deleted inserted replaced
349:0ddc495e8b83 350:d9ebca601847
    15 %index, putting page numbers of definitions in boldface
    15 %index, putting page numbers of definitions in boldface
    16 \newcommand\bold[1]{{\bf#1}}
    16 \newcommand\bold[1]{{\bf#1}}
    17 \newcommand\fnote[1]{#1n}
    17 \newcommand\fnote[1]{#1n}
    18 \newcommand\indexbold[1]{\index{#1|bold}}
    18 \newcommand\indexbold[1]{\index{#1|bold}}
    19 
    19 
       
    20 %for indexing constants, symbols, theorems, ...
       
    21 \newcommand\cdx[1]{{\tt#1}\index{#1@{\tt#1} constant}}
       
    22 \newcommand\sdx[1]{{\tt#1}\index{#1@{\tt#1} symbol}}
       
    23 
       
    24 \newcommand\tdx[1]{{\tt#1}\index{#1@{\tt#1} theorem}}
       
    25 \newcommand\tdxbold[1]{{\tt#1}\index{#1@{\tt#1} theorem|bold}}
       
    26 
       
    27 \newcommand\mltydx[1]{{\tt#1}\index{#1@{\tt#1} ML type}}
       
    28 \newcommand\xdx[1]{{\tt#1}\index{#1@{\tt#1} exception}}
       
    29 
       
    30 \newcommand\ndx[1]{{\tt#1}\index{#1@{\tt#1} nonterminal}}
       
    31 \newcommand\ndxbold[1]{{\tt#1}\index{#1@{\tt#1} nonterminal|bold}}
       
    32 
       
    33 \newcommand\cldx[1]{{\tt#1}\index{#1@{\tt#1} class}}
       
    34 \newcommand\tydx[1]{{\tt#1}\index{#1@{\tt#1} type}}
       
    35 \newcommand\thydx[1]{{\tt#1}\index{#1@{\tt#1} theory}}
       
    36 
    20 %for cross-references: 2nd argument (page number) is ignored
    37 %for cross-references: 2nd argument (page number) is ignored
    21 \newcommand\see[2]{{\it see \/}{#1}}
    38 \newcommand\see[2]{{\it see \/}{#1}}
    22 \newcommand\seealso[2]{{\it see also \/}{#1}}
    39 \newcommand\seealso[2]{{\it see also \/}{#1}}
    23 
    40 
    24 %set argument in \tt font; at the sime time, index using * prefix
    41 %set argument in \tt font; at the sime time, index using * prefix
       
    42 \newcommand\rmindex[1]{{#1}\index{#1}\@}
    25 \newcommand\ttindex[1]{{\tt#1}\index{*#1}\@}
    43 \newcommand\ttindex[1]{{\tt#1}\index{*#1}\@}
    26 \newcommand\ttindexbold[1]{{\tt#1}\index{*#1|bold}\@}
    44 \newcommand\ttindexbold[1]{{\tt#1}\index{*#1|bold}\@}
    27 
    45 
    28 %set argument in \bf font and index in ROMAN font (for definitions in text!)
    46 %set argument in \bf font and index in ROMAN font (for definitions in text!)
    29 \newcommand\bfindex[1]{{\bf#1}\index{#1|bold}\@}
    47 \newcommand\bfindex[1]{{\bf#1}\index{#1|bold}\@}
    83 \let\inter=\bigcap
   101 \let\inter=\bigcap
    84 \let\union=\bigcup
   102 \let\union=\bigcup
    85 
   103 
    86 \def\ML{{\sc ml}}
   104 \def\ML{{\sc ml}}
    87 \def\OBJ{{\sc obj}}
   105 \def\OBJ{{\sc obj}}
       
   106 \def\AST{{\sc ast}}
    88 
   107 
    89 \def\LCF{{\tt LCF}\@}
   108 \def\LCF{{\tt LCF}\@}
    90 \def\FOL{{\tt FOL}\@}
   109 \def\FOL{{\tt FOL}\@}
    91 \def\HOL{{\tt HOL}\@}
   110 \def\HOL{{\tt HOL}\@}
    92 \def\LK{{\tt LK}\@}
   111 \def\LK{{\tt LK}\@}
   101 \def\binvert{\mathcode`\|="226A}     %treat | like a binary operator
   120 \def\binvert{\mathcode`\|="226A}     %treat | like a binary operator
   102 
   121 
   103 %redefinition of \sloppy and \fussy to use \emergencystretch
   122 %redefinition of \sloppy and \fussy to use \emergencystretch
   104 \def\sloppy{\tolerance2000 \hfuzz.5pt \vfuzz.5pt \emergencystretch=15pt}
   123 \def\sloppy{\tolerance2000 \hfuzz.5pt \vfuzz.5pt \emergencystretch=15pt}
   105 \def\fussy{\tolerance200 \hfuzz.1pt \vfuzz.1pt \emergencystretch=0pt}
   124 \def\fussy{\tolerance200 \hfuzz.1pt \vfuzz.1pt \emergencystretch=0pt}
       
   125 
       
   126 %%%% \tt things
       
   127 
       
   128 \def\ttdescriptionlabel#1{\hspace\labelsep \tt #1}
       
   129 \def\ttdescription{\list{}{\labelwidth\z@ \itemindent-\leftmargin
       
   130        \let\makelabel\ttdescriptionlabel}}
       
   131 
       
   132 \let\endttdescription\endlist
   106 
   133 
   107 \chardef\ttilde=`\~     % A tilde for \tt font
   134 \chardef\ttilde=`\~     % A tilde for \tt font
   108 \chardef\ttback=`\\     % A backslash for \tt font
   135 \chardef\ttback=`\\     % A backslash for \tt font
   109 \chardef\ttlbrace=`\{   % A left brace for \tt font
   136 \chardef\ttlbrace=`\{   % A left brace for \tt font
   110 \chardef\ttrbrace=`\}   % A right brace for \tt font
   137 \chardef\ttrbrace=`\}   % A right brace for \tt font