doc-src/LaTeXsugar/Sugar/generated/mathpartir.sty
author kleing
Thu, 14 Apr 2005 08:52:46 +0200
changeset 15728 a6a74062ffb0
permissions -rw-r--r--
added Makefile and generated files to make document available for makedist
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
15728
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
     1
%%
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
     2
%% This is the original source file mathpar.sty
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
     3
%%
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
     4
%% Package `mathpar' to use with LaTeX 2e
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
     5
%% Copyright Didier Remy, all rights reserved.
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
     6
\NeedsTeXFormat{LaTeX2e}
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
     7
\ProvidesPackage{mathpartir}
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
     8
         [2001/23/02 v0.92 Math Paragraph for Type Inference Rules]
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
     9
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
    10
%%
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
    11
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
    12
%% Identification
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
    13
%% Preliminary declarations
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
    14
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
    15
\RequirePackage {keyval}
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
    16
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
    17
%% Options
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
    18
%% More declarations
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
    19
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
    20
%% PART I: Typesetting maths in paragraphe mode
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
    21
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
    22
\newdimen \mpr@tmpdim
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
    23
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
    24
% To ensure hevea \hva compatibility, \hva should expands to nothing 
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
    25
% in mathpar or in mathrule
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
    26
\let \mpr@hva \empty
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
    27
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
    28
%% normal paragraph parametters, should rather be taken dynamically
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
    29
\def \mpr@savepar {%
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
    30
  \edef \MathparNormalpar
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
    31
     {\noexpand \lineskiplimit \the\lineskiplimit
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
    32
      \noexpand \lineski \the\lineskip}%
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
    33
  }
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
    34
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
    35
\def \mpr@rulelineskip {\lineskiplimit=0.3em\lineskip=0.2em plus 0.1em}
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
    36
\def \mpr@lesslineskip {\lineskiplimit=0.6em\lineskip=0.5em plus 0.2em}
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
    37
\def \mpr@lineskip  {\lineskiplimit=1.2em\lineskip=1.2em plus 0.2em}
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
    38
\let \MathparLineskip \mpr@lineskip
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
    39
\def \mpr@paroptions {\MathparLineskip}
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
    40
\let \mpr@prebindings \relax
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
    41
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
    42
\newskip \mpr@andskip \mpr@andskip 2em plus 0.5fil minus 0.5em
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
    43
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
    44
\def \mpr@goodbreakand
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
    45
   {\hskip -\mpr@andskip  \penalty -1000\hskip \mpr@andskip}
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
    46
\def \mpr@and {\hskip \mpr@andskip}
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
    47
\def \mpr@andcr {\penalty 50\mpr@and}
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
    48
\def \mpr@cr {\penalty -10000\mpr@and}
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
    49
\def \mpr@eqno #1{\mpr@andcr #1\hskip 0em plus -1fil \penalty 10}
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
    50
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
    51
\def \mpr@bindings {%
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
    52
  \let \and \mpr@andcr
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
    53
  \let \par \mpr@andcr
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
    54
  \let \\\mpr@cr
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
    55
  \let \eqno \mpr@eqno
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
    56
  \let \hva \mpr@hva
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
    57
  } 
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
    58
\let \MathparBindings \mpr@bindings
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
    59
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
    60
\newenvironment{mathpar}[1][]
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
    61
  {$$\mpr@savepar \parskip 0em \hsize \linewidth \centering
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
    62
     \vbox \bgroup \mpr@prebindings \mpr@paroptions #1\ifmmode $\else
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
    63
     \noindent $\displaystyle\fi
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
    64
     \MathparBindings}
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
    65
  {\unskip \ifmmode $\fi\egroup $$\ignorespacesafterend}
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
    66
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
    67
% \def \math@mathpar #1{\setbox0 \hbox {$\displaystyle #1$}\ifnum
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
    68
%     \wd0 < \hsize  $$\box0$$\else \bmathpar #1\emathpar \fi}
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
    69
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
    70
%%% HOV BOXES
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
    71
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
    72
\def \mathvbox@ #1{\hbox \bgroup \mpr@normallineskip 
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
    73
  \vbox \bgroup \tabskip 0em \let \\ \cr
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
    74
  \halign \bgroup \hfil $##$\hfil\cr #1\crcr \egroup \egroup
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
    75
  \egroup}
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
    76
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
    77
\def \mathhvbox@ #1{\setbox0 \hbox {\let \\\qquad $#1$}\ifnum \wd0 < \hsize
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
    78
      \box0\else \mathvbox {#1}\fi}
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
    79
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
    80
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
    81
%% Part II -- operations on lists
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
    82
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
    83
\newtoks \mpr@lista
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
    84
\newtoks \mpr@listb
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
    85
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
    86
\long \def\mpr@cons #1\to#2{\mpr@lista {\\{#1}}\mpr@listb \expandafter
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
    87
{#2}\edef #2{\the \mpr@lista \the \mpr@listb}}
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
    88
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
    89
\long \def\mpr@snoc #1\to#2{\mpr@lista {\\{#1}}\mpr@listb \expandafter
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
    90
{#2}\edef #2{\the \mpr@listb\the\mpr@lista}}
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
    91
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
    92
\long \def \mpr@concat#1=#2\to#3{\mpr@lista \expandafter {#2}\mpr@listb
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
    93
\expandafter {#3}\edef #1{\the \mpr@listb\the\mpr@lista}}
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
    94
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
    95
\def \mpr@head #1\to #2{\expandafter \mpr@head@ #1\mpr@head@ #1#2}
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
    96
\long \def \mpr@head@ #1#2\mpr@head@ #3#4{\def #4{#1}\def#3{#2}}
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
    97
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
    98
\def \mpr@flatten #1\to #2{\expandafter \mpr@flatten@ #1\mpr@flatten@ #1#2}
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
    99
\long \def \mpr@flatten@ \\#1\\#2\mpr@flatten@ #3#4{\def #4{#1}\def #3{\\#2}}
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
   100
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
   101
\def \mpr@makelist #1\to #2{\def \mpr@all {#1}%
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
   102
   \mpr@lista {\\}\mpr@listb \expandafter {\mpr@all}\edef \mpr@all {\the
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
   103
   \mpr@lista \the \mpr@listb \the \mpr@lista}\let #2\empty 
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
   104
   \def \mpr@stripof ##1##2\mpr@stripend{\def \mpr@stripped{##2}}\loop
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
   105
     \mpr@flatten \mpr@all \to \mpr@one
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
   106
     \expandafter \mpr@snoc \mpr@one \to #2\expandafter \mpr@stripof
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
   107
     \mpr@all \mpr@stripend  
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
   108
     \ifx \mpr@stripped \empty \let \mpr@isempty 0\else \let \mpr@isempty 1\fi
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
   109
     \ifx 1\mpr@isempty
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
   110
   \repeat
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
   111
}
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
   112
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
   113
%% Part III -- Type inference rules
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
   114
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
   115
\def \mpr@rev #1\to #2{\let \mpr@tmp \empty
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
   116
   \def \\##1{\mpr@cons ##1\to \mpr@tmp}#1\let #2\mpr@tmp}
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
   117
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
   118
\newif \if@premisse
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
   119
\newbox \mpr@hlist
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
   120
\newbox \mpr@vlist
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
   121
\newif \ifmpr@center \mpr@centertrue
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
   122
\def \mpr@htovlist {%
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
   123
   \setbox \mpr@hlist
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
   124
      \hbox {\strut
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
   125
             \ifmpr@center \hskip -0.5\wd\mpr@hlist\fi
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
   126
             \unhbox \mpr@hlist}%
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
   127
   \setbox \mpr@vlist
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
   128
      \vbox {\if@premisse  \box \mpr@hlist \unvbox \mpr@vlist
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
   129
             \else \unvbox \mpr@vlist \box \mpr@hlist
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
   130
             \fi}%
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
   131
}
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
   132
% OLD version
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
   133
% \def \mpr@htovlist {%
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
   134
%    \setbox \mpr@hlist
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
   135
%       \hbox {\strut \hskip -0.5\wd\mpr@hlist \unhbox \mpr@hlist}%
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
   136
%    \setbox \mpr@vlist
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
   137
%       \vbox {\if@premisse  \box \mpr@hlist \unvbox \mpr@vlist
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
   138
%              \else \unvbox \mpr@vlist \box \mpr@hlist
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
   139
%              \fi}%
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
   140
% }
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
   141
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
   142
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
   143
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
   144
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
   145
\def \mpr@blank { }
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
   146
\def \mpr@hovbox #1#2{\hbox
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
   147
  \bgroup
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
   148
  \ifx #1T\@premissetrue
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
   149
  \else \ifx #1B\@premissefalse
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
   150
  \else
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
   151
     \PackageError{mathpartir}
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
   152
       {Premisse orientation should either be P or B}
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
   153
       {Fatal error in Package}%
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
   154
  \fi \fi
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
   155
  \def \@test {#2}\ifx \@test \mpr@blank\else
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
   156
  \setbox \mpr@hlist \hbox {}%
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
   157
  \setbox \mpr@vlist \vbox {}%
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
   158
  \if@premisse \let \snoc \mpr@cons \else \let \snoc \mpr@snoc \fi
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
   159
  \let \@hvlist \empty \let \@rev \empty
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
   160
  \mpr@tmpdim 0em
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
   161
  \expandafter \mpr@makelist #2\to \mpr@flat
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
   162
  \if@premisse \mpr@rev \mpr@flat \to \@rev \else \let \@rev \mpr@flat \fi
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
   163
  \def \\##1{%
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
   164
     \def \@test {##1}\ifx \@test \empty
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
   165
        \mpr@htovlist
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
   166
        \mpr@tmpdim 0em %%% last bug fix not extensively checked
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
   167
     \else
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
   168
      \setbox0 \hbox{$\displaystyle {##1}$}\relax
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
   169
      \advance \mpr@tmpdim by \wd0
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
   170
      %\mpr@tmpdim 1.02\mpr@tmpdim
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
   171
      \ifnum \mpr@tmpdim < \hsize
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
   172
         \ifnum \wd\mpr@hlist > 0
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
   173
           \if@premisse
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
   174
             \setbox \mpr@hlist \hbox {\unhbox0 \qquad \unhbox \mpr@hlist}%
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
   175
           \else
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
   176
             \setbox \mpr@hlist \hbox {\unhbox \mpr@hlist \qquad \unhbox0}%
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
   177
           \fi
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
   178
         \else 
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
   179
         \setbox \mpr@hlist \hbox {\unhbox0}%
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
   180
         \fi
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
   181
      \else
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
   182
         \ifnum \wd \mpr@hlist > 0
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
   183
            \mpr@htovlist 
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
   184
            \mpr@tmpdim \wd0
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
   185
         \fi
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
   186
         \setbox \mpr@hlist \hbox {\unhbox0}%
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
   187
      \fi
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
   188
      \advance \mpr@tmpdim by 2em
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
   189
   \fi
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
   190
   }%
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
   191
   \@rev
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
   192
   \mpr@htovlist
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
   193
   \ifmpr@center \hskip \wd\mpr@vlist\fi \box \mpr@vlist
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
   194
   \fi
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
   195
   \egroup
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
   196
}
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
   197
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
   198
%%% INFERENCE RULES
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
   199
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
   200
\@ifundefined{@@over}{%
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
   201
    \let\@@over\over % fallback if amsmath is not loaded
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
   202
    \let\@@overwithdelims\overwithdelims
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
   203
    \let\@@atop\atop \let\@@atopwithdelims\atopwithdelims
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
   204
    \let\@@above\above \let\@@abovewithdelims\abovewithdelims
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
   205
  }{}
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
   206
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
   207
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
   208
\def \mpr@@fraction #1#2{\hbox {\advance \hsize by -0.5em
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
   209
    $\displaystyle {#1\@@over #2}$}}
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
   210
\let \mpr@fraction \mpr@@fraction
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
   211
\def \mpr@@reduce #1#2{\hbox
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
   212
    {$\lower 0.01pt \mpr@@fraction {#1}{#2}\mkern -15mu\rightarrow$}}
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
   213
\def \mpr@infercenter #1{\vcenter {\mpr@hovbox{T}{#1}}}
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
   214
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
   215
\def \mpr@empty {}
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
   216
\def \mpr@inferrule
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
   217
  {\bgroup
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
   218
     \mpr@rulelineskip
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
   219
     \let \and \qquad
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
   220
     \let \hva \mpr@hva
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
   221
     \let \@rulename \mpr@empty
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
   222
     \let \@rule@options \mpr@empty
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
   223
     \mpr@inferrule@}
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
   224
\newcommand {\mpr@inferrule@}[3][]
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
   225
  {\everymath={\displaystyle}%       
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
   226
   \def \@test {#2}\ifx \empty \@test
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
   227
      \setbox0 \hbox {$\vcenter {\mpr@hovbox{B}{#3}}$}%
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
   228
   \else 
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
   229
   \def \@test {#3}\ifx \empty \@test
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
   230
      \setbox0 \hbox {$\vcenter {\mpr@hovbox{T}{#2}}$}%
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
   231
   \else
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
   232
   \setbox0 \mpr@fraction {\mpr@hovbox{T}{#2}}{\mpr@hovbox{B}{#3}}%
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
   233
   \fi \fi
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
   234
   \def \@test {#1}\ifx \@test\empty \box0
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
   235
   \else \vbox 
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
   236
%%% Suggestion de Francois pour les etiquettes longues
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
   237
%%%   {\hbox to \wd0 {\TirName {#1}\hfil}\box0}\fi
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
   238
      {\hbox {\TirName {#1}}\box0}\fi
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
   239
   \egroup}
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
   240
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
   241
\def \mpr@vdotfil #1{\vbox to #1{\leaders \hbox{$\cdot$} \vfil}}
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
   242
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
   243
% They are two forms
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
   244
% \mathrule [label]{[premisses}{conclusions}
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
   245
% or
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
   246
% \mathrule* [options]{[premisses}{conclusions}
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
   247
%
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
   248
% Premisses and conclusions are lists of elements separated by \\
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
   249
% Each \\ produces a break, attempting horizontal breaks if possible, 
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
   250
% and  vertical breaks if needed. 
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
   251
% 
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
   252
% An empty element obtained by \\\\ produces a vertical break in all cases. 
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
   253
%
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
   254
% The former rule is aligned on the fraction bar. 
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
   255
% The optional label appears on top of the rule
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
   256
% The second form to be used in a derivation tree is aligned on the last
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
   257
% line of its conclusion
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
   258
% 
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
   259
% The second form can be parameterized, using the key=val interface. The
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
   260
% folloiwng keys are recognized:
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
   261
%       
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
   262
%  width                set the width of the rule to val
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
   263
%  narrower             set the width of the rule to val\hsize
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
   264
%  before               execute val at the beginning/left
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
   265
%  lab                  put a label [Val] on top of the rule
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
   266
%  lskip                add negative skip on the right
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
   267
%  llab                 put a left label [Val],  ignoring its width 
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
   268
%  left                 put a left label [Val]
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
   269
%  right                put a right label [Val]
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
   270
%  rlab                 put a right label [Val], ignoring its width
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
   271
%  rskip                add negative skip on the left
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
   272
%  vdots                lift the rule by val and fill vertical space with dots
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
   273
%  after                execute val at the end/right
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
   274
%  
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
   275
%  Note that most options must come in this order to avoid strange
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
   276
%  typesetting (in particular  lskip must preceed left and llab and
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
   277
%  rskip must follow rlab or right; vdots must come last or be followed by
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
   278
%  rskip. 
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
   279
%  
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
   280
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
   281
\define@key {mprset}{flushleft}[]{\mpr@centerfalse}
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
   282
\define@key {mprset}{center}[]{\mpr@centertrue}
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
   283
\def \mprset #1{\setkeys{mprset}{#1}}
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
   284
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
   285
\newbox \mpr@right
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
   286
\define@key {mpr}{flushleft}[]{\mpr@centerfalse}
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
   287
\define@key {mpr}{center}[]{\mpr@centertrue}
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
   288
\define@key {mpr}{left}{\setbox0 \hbox {$\TirName {#1}\;$}\relax
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
   289
     \advance \hsize by -\wd0\box0}
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
   290
\define@key {mpr}{width}{\hsize #1}
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
   291
\define@key {mpr}{before}{#1}
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
   292
\define@key {mpr}{lab}{\def \mpr@rulename {[#1]}}
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
   293
\define@key {mpr}{Lab}{\def \mpr@rulename {#1}}
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
   294
\define@key {mpr}{narrower}{\hsize #1\hsize}
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
   295
\define@key {mpr}{leftskip}{\hskip -#1}
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
   296
\define@key {mpr}{reduce}[]{\let \mpr@fraction \mpr@@reduce}
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
   297
\define@key {mpr}{rightskip}
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
   298
  {\setbox \mpr@right \hbox {\unhbox \mpr@right \hskip -#1}}
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
   299
\define@key {mpr}{left}{\setbox0 \hbox {$\TirName {#1}\;$}\relax
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
   300
     \advance \hsize by -\wd0\box0}
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
   301
\define@key {mpr}{Left}{\llap{$\TirName {#1}\;$}}
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
   302
\define@key {mpr}{right}
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
   303
  {\setbox0 \hbox {$\;\TirName {#1}$}\relax \advance \hsize by -\wd0
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
   304
   \setbox \mpr@right \hbox {\unhbox \mpr@right \unhbox0}}
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
   305
\define@key {mpr}{Right}
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
   306
  {\setbox \mpr@right \hbox {\unhbox \mpr@right \rlap {$\;\TirName {#1}$}}}
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
   307
\define@key {mpr}{vdots}{\def \mpr@vdots {\@@atop \mpr@vdotfil{#1}}}
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
   308
\define@key {mpr}{after}{\edef \mpr@after {\mpr@after #1}}
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
   309
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
   310
\newdimen \rule@dimen
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
   311
\newcommand \mpr@inferstar@ [3][]{\setbox0
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
   312
  \hbox {\let \mpr@rulename \mpr@empty \let \mpr@vdots \relax
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
   313
         \setbox \mpr@right \hbox{}%
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
   314
         $\setkeys{mpr}{#1}%
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
   315
          \ifx \mpr@rulename \mpr@empty \mpr@inferrule {#2}{#3}\else
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
   316
          \mpr@inferrule [{\mpr@rulename}]{#2}{#3}\fi
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
   317
          \box \mpr@right \mpr@vdots$}
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
   318
  \setbox1 \hbox {\strut}
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
   319
  \rule@dimen \dp0 \advance \rule@dimen by -\dp1
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
   320
  \raise \rule@dimen \box0}
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
   321
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
   322
\def \mpr@infer {\@ifnextchar *{\mpr@inferstar}{\mpr@inferrule}}
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
   323
\newcommand \mpr@err@skipargs[3][]{}
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
   324
\def \mpr@inferstar*{\ifmmode 
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
   325
    \let \@do \mpr@inferstar@
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
   326
  \else 
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
   327
    \let \@do \mpr@err@skipargs
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
   328
    \PackageError {mathpartir}
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
   329
      {\string\inferrule* can only be used in math mode}{}%
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
   330
  \fi \@do}
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
   331
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
   332
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
   333
%%% Exports
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
   334
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
   335
% Envirnonment mathpar
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
   336
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
   337
\let \inferrule \mpr@infer
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
   338
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
   339
% make a short name \infer is not already defined
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
   340
\@ifundefined {infer}{\let \infer \mpr@infer}{}
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
   341
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
   342
\def \tir@name #1{\hbox {\small \sc #1}}
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
   343
\let \TirName \tir@name
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
   344
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
   345
%%% Other Exports
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
   346
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
   347
% \let \listcons \mpr@cons
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
   348
% \let \listsnoc \mpr@snoc
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
   349
% \let \listhead \mpr@head
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
   350
% \let \listmake \mpr@makelist
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
   351
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
   352
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
   353
\endinput
a6a74062ffb0 added Makefile and generated files to make document available for makedist
kleing
parents:
diff changeset
   354