# HG changeset patch
# User wenzelm
# Date 1599825856 -7200
# Node ID dc51115fa4aad5f08e46bb5c9651cc3b04101205
# Parent  8c5b8d7999bd0218bcd8a14e41301787d8a212fa
prefer current mathpartir.sty from underlying TeX distribution;

diff -r 8c5b8d7999bd -r dc51115fa4aa src/Doc/Functions/document/mathpartir.sty
--- a/src/Doc/Functions/document/mathpartir.sty	Fri Sep 11 13:54:22 2020 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,421 +0,0 @@
-%  Mathpartir --- Math Paragraph for Typesetting Inference Rules
-%
-%  Copyright (C) 2001, 2002, 2003, 2004, 2005 Didier Rémy
-%
-%  Author         : Didier Remy 
-%  Version        : 1.2.0
-%  Bug Reports    : to author
-%  Web Site       : http://pauillac.inria.fr/~remy/latex/
-% 
-%  Mathpartir is free software; you can redistribute it and/or modify
-%  it under the terms of the GNU General Public License as published by
-%  the Free Software Foundation; either version 2, or (at your option)
-%  any later version.
-%  
-%  Mathpartir is distributed in the hope that it will be useful,
-%  but WITHOUT ANY WARRANTY; without even the implied warranty of
-%  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
-%  GNU General Public License for more details 
-%  (http://pauillac.inria.fr/~remy/license/GPL).
-%
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-%  File mathpartir.sty (LaTeX macros)
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-
-\NeedsTeXFormat{LaTeX2e}
-\ProvidesPackage{mathpartir}
-    [2005/12/20 version 1.2.0 Math Paragraph for Typesetting Inference Rules]
-
-%%
-
-%% Identification
-%% Preliminary declarations
-
-\RequirePackage {keyval}
-
-%% Options
-%% More declarations
-
-%% PART I: Typesetting maths in paragraphe mode
-
-\newdimen \mpr@tmpdim
-
-% To ensure hevea \hva compatibility, \hva should expands to nothing 
-% in mathpar or in inferrule
-\let \mpr@hva \empty
-
-%% normal paragraph parametters, should rather be taken dynamically
-\def \mpr@savepar {%
-  \edef \MathparNormalpar
-     {\noexpand \lineskiplimit \the\lineskiplimit
-      \noexpand \lineskip \the\lineskip}%
-  }
-
-\def \mpr@rulelineskip {\lineskiplimit=0.3em\lineskip=0.2em plus 0.1em}
-\def \mpr@lesslineskip {\lineskiplimit=0.6em\lineskip=0.5em plus 0.2em}
-\def \mpr@lineskip  {\lineskiplimit=1.2em\lineskip=1.2em plus 0.2em}
-\let \MathparLineskip \mpr@lineskip
-\def \mpr@paroptions {\MathparLineskip}
-\let \mpr@prebindings \relax
-
-\newskip \mpr@andskip \mpr@andskip 2em plus 0.5fil minus 0.5em
-
-\def \mpr@goodbreakand
-   {\hskip -\mpr@andskip  \penalty -1000\hskip \mpr@andskip}
-\def \mpr@and {\hskip \mpr@andskip}
-\def \mpr@andcr {\penalty 50\mpr@and}
-\def \mpr@cr {\penalty -10000\mpr@and}
-\def \mpr@eqno #1{\mpr@andcr #1\hskip 0em plus -1fil \penalty 10}
-
-\def \mpr@bindings {%
-  \let \and \mpr@andcr
-  \let \par \mpr@andcr
-  \let \\\mpr@cr
-  \let \eqno \mpr@eqno
-  \let \hva \mpr@hva
-  } 
-\let \MathparBindings \mpr@bindings
-
-% \@ifundefined {ignorespacesafterend}
-%    {\def \ignorespacesafterend {\aftergroup \ignorespaces}
-
-\newenvironment{mathpar}[1][]
-  {$$\mpr@savepar \parskip 0em \hsize \linewidth \centering
-     \vbox \bgroup \mpr@prebindings \mpr@paroptions #1\ifmmode $\else
-     \noindent $\displaystyle\fi
-     \MathparBindings}
-  {\unskip \ifmmode $\fi\egroup $$\ignorespacesafterend}
-
-% \def \math@mathpar #1{\setbox0 \hbox {$\displaystyle #1$}\ifnum
-%     \wd0 < \hsize  $$\box0$$\else \bmathpar #1\emathpar \fi}
-
-%%% HOV BOXES
-
-\def \mathvbox@ #1{\hbox \bgroup \mpr@normallineskip 
-  \vbox \bgroup \tabskip 0em \let \\ \cr
-  \halign \bgroup \hfil $##$\hfil\cr #1\crcr \egroup \egroup
-  \egroup}
-
-\def \mathhvbox@ #1{\setbox0 \hbox {\let \\\qquad $#1$}\ifnum \wd0 < \hsize
-      \box0\else \mathvbox {#1}\fi}
-
-
-%% Part II -- operations on lists
-
-\newtoks \mpr@lista
-\newtoks \mpr@listb
-
-\long \def\mpr@cons #1\mpr@to#2{\mpr@lista {\\{#1}}\mpr@listb \expandafter
-{#2}\edef #2{\the \mpr@lista \the \mpr@listb}}
-
-\long \def\mpr@snoc #1\mpr@to#2{\mpr@lista {\\{#1}}\mpr@listb \expandafter
-{#2}\edef #2{\the \mpr@listb\the\mpr@lista}}
-
-\long \def \mpr@concat#1=#2\mpr@to#3{\mpr@lista \expandafter {#2}\mpr@listb
-\expandafter {#3}\edef #1{\the \mpr@listb\the\mpr@lista}}
-
-\def \mpr@head #1\mpr@to #2{\expandafter \mpr@head@ #1\mpr@head@ #1#2}
-\long \def \mpr@head@ #1#2\mpr@head@ #3#4{\def #4{#1}\def#3{#2}}
-
-\def \mpr@flatten #1\mpr@to #2{\expandafter \mpr@flatten@ #1\mpr@flatten@ #1#2}
-\long \def \mpr@flatten@ \\#1\\#2\mpr@flatten@ #3#4{\def #4{#1}\def #3{\\#2}}
-
-\def \mpr@makelist #1\mpr@to #2{\def \mpr@all {#1}%
-   \mpr@lista {\\}\mpr@listb \expandafter {\mpr@all}\edef \mpr@all {\the
-   \mpr@lista \the \mpr@listb \the \mpr@lista}\let #2\empty 
-   \def \mpr@stripof ##1##2\mpr@stripend{\def \mpr@stripped{##2}}\loop
-     \mpr@flatten \mpr@all \mpr@to \mpr@one
-     \expandafter \mpr@snoc \mpr@one \mpr@to #2\expandafter \mpr@stripof
-     \mpr@all \mpr@stripend  
-     \ifx \mpr@stripped \empty \let \mpr@isempty 0\else \let \mpr@isempty 1\fi
-     \ifx 1\mpr@isempty
-   \repeat
-}
-
-\def \mpr@rev #1\mpr@to #2{\let \mpr@tmp \empty
-   \def \\##1{\mpr@cons ##1\mpr@to \mpr@tmp}#1\let #2\mpr@tmp}
-
-%% Part III -- Type inference rules
-
-\newif \if@premisse
-\newbox \mpr@hlist
-\newbox \mpr@vlist
-\newif \ifmpr@center \mpr@centertrue
-\def \mpr@htovlist {%
-   \setbox \mpr@hlist
-      \hbox {\strut
-             \ifmpr@center \hskip -0.5\wd\mpr@hlist\fi
-             \unhbox \mpr@hlist}%
-   \setbox \mpr@vlist
-      \vbox {\if@premisse  \box \mpr@hlist \unvbox \mpr@vlist
-             \else \unvbox \mpr@vlist \box \mpr@hlist
-             \fi}%
-}
-% OLD version
-% \def \mpr@htovlist {%
-%    \setbox \mpr@hlist
-%       \hbox {\strut \hskip -0.5\wd\mpr@hlist \unhbox \mpr@hlist}%
-%    \setbox \mpr@vlist
-%       \vbox {\if@premisse  \box \mpr@hlist \unvbox \mpr@vlist
-%              \else \unvbox \mpr@vlist \box \mpr@hlist
-%              \fi}%
-% }
-
-\def \mpr@item #1{$\displaystyle #1$}
-\def \mpr@sep{2em}
-\def \mpr@blank { }
-\def \mpr@hovbox #1#2{\hbox
-  \bgroup
-  \ifx #1T\@premissetrue
-  \else \ifx #1B\@premissefalse
-  \else
-     \PackageError{mathpartir}
-       {Premisse orientation should either be T or B}
-       {Fatal error in Package}%
-  \fi \fi
-  \def \@test {#2}\ifx \@test \mpr@blank\else
-  \setbox \mpr@hlist \hbox {}%
-  \setbox \mpr@vlist \vbox {}%
-  \if@premisse \let \snoc \mpr@cons \else \let \snoc \mpr@snoc \fi
-  \let \@hvlist \empty \let \@rev \empty
-  \mpr@tmpdim 0em
-  \expandafter \mpr@makelist #2\mpr@to \mpr@flat
-  \if@premisse \mpr@rev \mpr@flat \mpr@to \@rev \else \let \@rev \mpr@flat \fi
-  \def \\##1{%
-     \def \@test {##1}\ifx \@test \empty
-        \mpr@htovlist
-        \mpr@tmpdim 0em %%% last bug fix not extensively checked
-     \else
-      \setbox0 \hbox{\mpr@item {##1}}\relax
-      \advance \mpr@tmpdim by \wd0
-      %\mpr@tmpdim 1.02\mpr@tmpdim
-      \ifnum \mpr@tmpdim < \hsize
-         \ifnum \wd\mpr@hlist > 0
-           \if@premisse
-             \setbox \mpr@hlist 
-                \hbox {\unhbox0 \hskip \mpr@sep \unhbox \mpr@hlist}%
-           \else
-             \setbox \mpr@hlist
-                \hbox {\unhbox \mpr@hlist  \hskip \mpr@sep \unhbox0}%
-           \fi
-         \else 
-         \setbox \mpr@hlist \hbox {\unhbox0}%
-         \fi
-      \else
-         \ifnum \wd \mpr@hlist > 0
-            \mpr@htovlist 
-            \mpr@tmpdim \wd0
-         \fi
-         \setbox \mpr@hlist \hbox {\unhbox0}%
-      \fi
-      \advance \mpr@tmpdim by \mpr@sep
-   \fi
-   }%
-   \@rev
-   \mpr@htovlist
-   \ifmpr@center \hskip \wd\mpr@vlist\fi \box \mpr@vlist
-   \fi
-   \egroup
-}
-
-%%% INFERENCE RULES
-
-\@ifundefined{@@over}{%
-    \let\@@over\over % fallback if amsmath is not loaded
-    \let\@@overwithdelims\overwithdelims
-    \let\@@atop\atop \let\@@atopwithdelims\atopwithdelims
-    \let\@@above\above \let\@@abovewithdelims\abovewithdelims
-  }{}
-
-%% The default
-
-\def \mpr@@fraction #1#2{\hbox {\advance \hsize by -0.5em
-    $\displaystyle {#1\mpr@over #2}$}}
-\let \mpr@fraction \mpr@@fraction
-
-%% A generic solution to arrow
-
-\def \mpr@make@fraction #1#2#3#4#5{\hbox {%
-     \def \mpr@tail{#1}%
-     \def \mpr@body{#2}%
-     \def \mpr@head{#3}%
-     \setbox1=\hbox{$#4$}\setbox2=\hbox{$#5$}%
-     \setbox3=\hbox{$\mkern -3mu\mpr@body\mkern -3mu$}%
-     \setbox3=\hbox{$\mkern -3mu \mpr@body\mkern -3mu$}%
-     \dimen0=\dp1\advance\dimen0 by \ht3\relax\dp1\dimen0\relax
-     \dimen0=\ht2\advance\dimen0 by \dp3\relax\ht2\dimen0\relax
-     \setbox0=\hbox {$\box1 \@@atop \box2$}%
-     \dimen0=\wd0\box0
-     \box0 \hskip -\dimen0\relax
-     \hbox to \dimen0 {$%
-       \mathrel{\mpr@tail}\joinrel
-       \xleaders\hbox{\copy3}\hfil\joinrel\mathrel{\mpr@head}%
-     $}}}
-
-%% Old stuff should be removed in next version
-\def \mpr@@reduce #1#2{\hbox
-    {$\lower 0.01pt \mpr@@fraction {#1}{#2}\mkern -15mu\rightarrow$}}
-\def \mpr@@rewrite #1#2#3{\hbox
-    {$\lower 0.01pt \mpr@@fraction {#2}{#3}\mkern -8mu#1$}}
-\def \mpr@infercenter #1{\vcenter {\mpr@hovbox{T}{#1}}}
-
-\def \mpr@empty {}
-\def \mpr@inferrule
-  {\bgroup
-     \ifnum \linewidth<\hsize \hsize \linewidth\fi
-     \mpr@rulelineskip
-     \let \and \qquad
-     \let \hva \mpr@hva
-     \let \@rulename \mpr@empty
-     \let \@rule@options \mpr@empty
-     \let \mpr@over \@@over
-     \mpr@inferrule@}
-\newcommand {\mpr@inferrule@}[3][]
-  {\everymath={\displaystyle}%       
-   \def \@test {#2}\ifx \empty \@test
-      \setbox0 \hbox {$\vcenter {\mpr@hovbox{B}{#3}}$}%
-   \else 
-   \def \@test {#3}\ifx \empty \@test
-      \setbox0 \hbox {$\vcenter {\mpr@hovbox{T}{#2}}$}%
-   \else
-   \setbox0 \mpr@fraction {\mpr@hovbox{T}{#2}}{\mpr@hovbox{B}{#3}}%
-   \fi \fi
-   \def \@test {#1}\ifx \@test\empty \box0
-   \else \vbox 
-%%% Suggestion de Francois pour les etiquettes longues
-%%%   {\hbox to \wd0 {\RefTirName {#1}\hfil}\box0}\fi
-      {\hbox {\RefTirName {#1}}\box0}\fi
-   \egroup}
-
-\def \mpr@vdotfil #1{\vbox to #1{\leaders \hbox{$\cdot$} \vfil}}
-
-% They are two forms
-% \inferrule [label]{[premisses}{conclusions}
-% or
-% \inferrule* [options]{[premisses}{conclusions}
-%
-% Premisses and conclusions are lists of elements separated by \\
-% Each \\ produces a break, attempting horizontal breaks if possible, 
-% and  vertical breaks if needed. 
-% 
-% An empty element obtained by \\\\ produces a vertical break in all cases. 
-%
-% The former rule is aligned on the fraction bar. 
-% The optional label appears on top of the rule
-% The second form to be used in a derivation tree is aligned on the last
-% line of its conclusion
-% 
-% The second form can be parameterized, using the key=val interface. The
-% folloiwng keys are recognized:
-%       
-%  width                set the width of the rule to val
-%  narrower             set the width of the rule to val\hsize
-%  before               execute val at the beginning/left
-%  lab                  put a label [Val] on top of the rule
-%  lskip                add negative skip on the right
-%  left                 put a left label [Val]
-%  Left                 put a left label [Val],  ignoring its width 
-%  right                put a right label [Val]
-%  Right                put a right label [Val], ignoring its width
-%  leftskip             skip negative space on the left-hand side
-%  rightskip            skip negative space on the right-hand side
-%  vdots                lift the rule by val and fill vertical space with dots
-%  after                execute val at the end/right
-%  
-%  Note that most options must come in this order to avoid strange
-%  typesetting (in particular  leftskip must preceed left and Left and
-%  rightskip must follow Right or right; vdots must come last 
-%  or be only followed by rightskip. 
-%  
-
-%% Keys that make sence in all kinds of rules
-\def \mprset #1{\setkeys{mprset}{#1}}
-\define@key {mprset}{flushleft}[]{\mpr@centerfalse}
-\define@key {mprset}{center}[]{\mpr@centertrue}
-\define@key {mprset}{rewrite}[]{\let \mpr@fraction \mpr@@rewrite}
-\define@key {mprset}{myfraction}[]{\let \mpr@fraction #1}
-\define@key {mprset}{fraction}[]{\def \mpr@fraction {\mpr@make@fraction #1}}
-
-\newbox \mpr@right
-\define@key {mpr}{flushleft}[]{\mpr@centerfalse}
-\define@key {mpr}{center}[]{\mpr@centertrue}
-\define@key {mpr}{rewrite}[]{\let \mpr@fraction \mpr@@rewrite}
-\define@key {mpr}{myfraction}[]{\let \mpr@fraction #1}
-\define@key {mpr}{fraction}[]{\def \mpr@fraction {\mpr@make@fraction #1}}
-\define@key {mpr}{left}{\setbox0 \hbox {$\TirName {#1}\;$}\relax
-     \advance \hsize by -\wd0\box0}
-\define@key {mpr}{width}{\hsize #1}
-\define@key {mpr}{sep}{\def\mpr@sep{#1}}
-\define@key {mpr}{before}{#1}
-\define@key {mpr}{lab}{\let \RefTirName \TirName \def \mpr@rulename {#1}}
-\define@key {mpr}{Lab}{\let \RefTirName \TirName \def \mpr@rulename {#1}}
-\define@key {mpr}{narrower}{\hsize #1\hsize}
-\define@key {mpr}{leftskip}{\hskip -#1}
-\define@key {mpr}{reduce}[]{\let \mpr@fraction \mpr@@reduce}
-\define@key {mpr}{rightskip}
-  {\setbox \mpr@right \hbox {\unhbox \mpr@right \hskip -#1}}
-\define@key {mpr}{LEFT}{\setbox0 \hbox {$#1$}\relax
-     \advance \hsize by -\wd0\box0}
-\define@key {mpr}{left}{\setbox0 \hbox {$\TirName {#1}\;$}\relax
-     \advance \hsize by -\wd0\box0}
-\define@key {mpr}{Left}{\llap{$\TirName {#1}\;$}}
-\define@key {mpr}{right}
-  {\setbox0 \hbox {$\;\TirName {#1}$}\relax \advance \hsize by -\wd0
-   \setbox \mpr@right \hbox {\unhbox \mpr@right \unhbox0}}
-\define@key {mpr}{RIGHT}
-  {\setbox0 \hbox {$#1$}\relax \advance \hsize by -\wd0
-   \setbox \mpr@right \hbox {\unhbox \mpr@right \unhbox0}}
-\define@key {mpr}{Right}
-  {\setbox \mpr@right \hbox {\unhbox \mpr@right \rlap {$\;\TirName {#1}$}}}
-\define@key {mpr}{vdots}{\def \mpr@vdots {\@@atop \mpr@vdotfil{#1}}}
-\define@key {mpr}{after}{\edef \mpr@after {\mpr@after #1}}
-
-\newdimen \rule@dimen
-\newcommand \mpr@inferstar@ [3][]{\setbox0
-  \hbox {\let \mpr@rulename \mpr@empty \let \mpr@vdots \relax
-         \setbox \mpr@right \hbox{}%
-         $\setkeys{mpr}{#1}%
-          \ifx \mpr@rulename \mpr@empty \mpr@inferrule {#2}{#3}\else
-          \mpr@inferrule [{\mpr@rulename}]{#2}{#3}\fi
-          \box \mpr@right \mpr@vdots$}
-  \setbox1 \hbox {\strut}
-  \rule@dimen \dp0 \advance \rule@dimen by -\dp1
-  \raise \rule@dimen \box0}
-
-\def \mpr@infer {\@ifnextchar *{\mpr@inferstar}{\mpr@inferrule}}
-\newcommand \mpr@err@skipargs[3][]{}
-\def \mpr@inferstar*{\ifmmode 
-    \let \@do \mpr@inferstar@
-  \else 
-    \let \@do \mpr@err@skipargs
-    \PackageError {mathpartir}
-      {\string\inferrule* can only be used in math mode}{}%
-  \fi \@do}
-
-
-%%% Exports
-
-% Envirnonment mathpar
-
-\let \inferrule \mpr@infer
-
-% make a short name \infer is not already defined
-\@ifundefined {infer}{\let \infer \mpr@infer}{}
-
-\def \TirNameStyle #1{\small \textsc{#1}}
-\def \tir@name #1{\hbox {\small \TirNameStyle{#1}}}
-\let \TirName \tir@name
-\let \DefTirName \TirName
-\let \RefTirName \TirName
-
-%%% Other Exports
-
-% \let \listcons \mpr@cons
-% \let \listsnoc \mpr@snoc
-% \let \listhead \mpr@head
-% \let \listmake \mpr@makelist
-
-
-
-
-\endinput
diff -r 8c5b8d7999bd -r dc51115fa4aa src/Doc/Prog_Prove/document/mathpartir.sty
--- a/src/Doc/Prog_Prove/document/mathpartir.sty	Fri Sep 11 13:54:22 2020 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,388 +0,0 @@
-%  Mathpartir --- Math Paragraph for Typesetting Inference Rules
-%
-%  Copyright (C) 2001, 2002, 2003 Didier Rémy
-%
-%  Author         : Didier Remy 
-%  Version        : 1.1.1
-%  Bug Reports    : to author
-%  Web Site       : http://pauillac.inria.fr/~remy/latex/
-% 
-%  WhizzyTeX is free software; you can redistribute it and/or modify
-%  it under the terms of the GNU General Public License as published by
-%  the Free Software Foundation; either version 2, or (at your option)
-%  any later version.
-%  
-%  Mathpartir is distributed in the hope that it will be useful,
-%  but WITHOUT ANY WARRANTY; without even the implied warranty of
-%  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
-%  GNU General Public License for more details 
-%  (http://pauillac.inria.fr/~remy/license/GPL).
-%
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-%  File mathpartir.sty (LaTeX macros)
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-
-\NeedsTeXFormat{LaTeX2e}
-\ProvidesPackage{mathpartir}
-    [2003/07/10 version 1.1.1 Math Paragraph for Typesetting Inference Rules]
-
-%%
-
-%% Identification
-%% Preliminary declarations
-
-\RequirePackage {keyval}
-
-%% Options
-%% More declarations
-
-%% PART I: Typesetting maths in paragraphe mode
-
-\newdimen \mpr@tmpdim
-
-% To ensure hevea \hva compatibility, \hva should expands to nothing 
-% in mathpar or in inferrule
-\let \mpr@hva \empty
-
-%% normal paragraph parametters, should rather be taken dynamically
-\def \mpr@savepar {%
-  \edef \MathparNormalpar
-     {\noexpand \lineskiplimit \the\lineskiplimit
-      \noexpand \lineskip \the\lineskip}%
-  }
-
-\def \mpr@rulelineskip {\lineskiplimit=0.3em\lineskip=0.2em plus 0.1em}
-\def \mpr@lesslineskip {\lineskiplimit=0.6em\lineskip=0.5em plus 0.2em}
-\def \mpr@lineskip  {\lineskiplimit=1.2em\lineskip=1.2em plus 0.2em}
-\let \MathparLineskip \mpr@lineskip
-\def \mpr@paroptions {\MathparLineskip}
-\let \mpr@prebindings \relax
-
-\newskip \mpr@andskip \mpr@andskip 2em plus 0.5fil minus 0.5em
-
-\def \mpr@goodbreakand
-   {\hskip -\mpr@andskip  \penalty -1000\hskip \mpr@andskip}
-\def \mpr@and {\hskip \mpr@andskip}
-\def \mpr@andcr {\penalty 50\mpr@and}
-\def \mpr@cr {\penalty -10000\mpr@and}
-\def \mpr@eqno #1{\mpr@andcr #1\hskip 0em plus -1fil \penalty 10}
-
-\def \mpr@bindings {%
-  \let \and \mpr@andcr
-  \let \par \mpr@andcr
-  \let \\\mpr@cr
-  \let \eqno \mpr@eqno
-  \let \hva \mpr@hva
-  } 
-\let \MathparBindings \mpr@bindings
-
-% \@ifundefined {ignorespacesafterend}
-%    {\def \ignorespacesafterend {\aftergroup \ignorespaces}
-
-\newenvironment{mathpar}[1][]
-  {$$\mpr@savepar \parskip 0em \hsize \linewidth \centering
-     \vbox \bgroup \mpr@prebindings \mpr@paroptions #1\ifmmode $\else
-     \noindent $\displaystyle\fi
-     \MathparBindings}
-  {\unskip \ifmmode $\fi\egroup $$\ignorespacesafterend}
-
-% \def \math@mathpar #1{\setbox0 \hbox {$\displaystyle #1$}\ifnum
-%     \wd0 < \hsize  $$\box0$$\else \bmathpar #1\emathpar \fi}
-
-%%% HOV BOXES
-
-\def \mathvbox@ #1{\hbox \bgroup \mpr@normallineskip 
-  \vbox \bgroup \tabskip 0em \let \\ \cr
-  \halign \bgroup \hfil $##$\hfil\cr #1\crcr \egroup \egroup
-  \egroup}
-
-\def \mathhvbox@ #1{\setbox0 \hbox {\let \\\qquad $#1$}\ifnum \wd0 < \hsize
-      \box0\else \mathvbox {#1}\fi}
-
-
-%% Part II -- operations on lists
-
-\newtoks \mpr@lista
-\newtoks \mpr@listb
-
-\long \def\mpr@cons #1\mpr@to#2{\mpr@lista {\\{#1}}\mpr@listb \expandafter
-{#2}\edef #2{\the \mpr@lista \the \mpr@listb}}
-
-\long \def\mpr@snoc #1\mpr@to#2{\mpr@lista {\\{#1}}\mpr@listb \expandafter
-{#2}\edef #2{\the \mpr@listb\the\mpr@lista}}
-
-\long \def \mpr@concat#1=#2\mpr@to#3{\mpr@lista \expandafter {#2}\mpr@listb
-\expandafter {#3}\edef #1{\the \mpr@listb\the\mpr@lista}}
-
-\def \mpr@head #1\mpr@to #2{\expandafter \mpr@head@ #1\mpr@head@ #1#2}
-\long \def \mpr@head@ #1#2\mpr@head@ #3#4{\def #4{#1}\def#3{#2}}
-
-\def \mpr@flatten #1\mpr@to #2{\expandafter \mpr@flatten@ #1\mpr@flatten@ #1#2}
-\long \def \mpr@flatten@ \\#1\\#2\mpr@flatten@ #3#4{\def #4{#1}\def #3{\\#2}}
-
-\def \mpr@makelist #1\mpr@to #2{\def \mpr@all {#1}%
-   \mpr@lista {\\}\mpr@listb \expandafter {\mpr@all}\edef \mpr@all {\the
-   \mpr@lista \the \mpr@listb \the \mpr@lista}\let #2\empty 
-   \def \mpr@stripof ##1##2\mpr@stripend{\def \mpr@stripped{##2}}\loop
-     \mpr@flatten \mpr@all \mpr@to \mpr@one
-     \expandafter \mpr@snoc \mpr@one \mpr@to #2\expandafter \mpr@stripof
-     \mpr@all \mpr@stripend  
-     \ifx \mpr@stripped \empty \let \mpr@isempty 0\else \let \mpr@isempty 1\fi
-     \ifx 1\mpr@isempty
-   \repeat
-}
-
-%% Part III -- Type inference rules
-
-\def \mpr@rev #1\mpr@to #2{\let \mpr@tmp \empty
-   \def \\##1{\mpr@cons ##1\mpr@to \mpr@tmp}#1\let #2\mpr@tmp}
-
-\newif \if@premisse
-\newbox \mpr@hlist
-\newbox \mpr@vlist
-\newif \ifmpr@center \mpr@centertrue
-\def \mpr@htovlist {%
-   \setbox \mpr@hlist
-      \hbox {\strut
-             \ifmpr@center \hskip -0.5\wd\mpr@hlist\fi
-             \unhbox \mpr@hlist}%
-   \setbox \mpr@vlist
-      \vbox {\if@premisse  \box \mpr@hlist \unvbox \mpr@vlist
-             \else \unvbox \mpr@vlist \box \mpr@hlist
-             \fi}%
-}
-% OLD version
-% \def \mpr@htovlist {%
-%    \setbox \mpr@hlist
-%       \hbox {\strut \hskip -0.5\wd\mpr@hlist \unhbox \mpr@hlist}%
-%    \setbox \mpr@vlist
-%       \vbox {\if@premisse  \box \mpr@hlist \unvbox \mpr@vlist
-%              \else \unvbox \mpr@vlist \box \mpr@hlist
-%              \fi}%
-% }
-
-\def \mpr@sep{1.5em}
-\def \mpr@blank { }
-\def \mpr@hovbox #1#2{\hbox
-  \bgroup
-  \ifx #1T\@premissetrue
-  \else \ifx #1B\@premissefalse
-  \else
-     \PackageError{mathpartir}
-       {Premisse orientation should either be P or B}
-       {Fatal error in Package}%
-  \fi \fi
-  \def \@test {#2}\ifx \@test \mpr@blank\else
-  \setbox \mpr@hlist \hbox {}%
-  \setbox \mpr@vlist \vbox {}%
-  \if@premisse \let \snoc \mpr@cons \else \let \snoc \mpr@snoc \fi
-  \let \@hvlist \empty \let \@rev \empty
-  \mpr@tmpdim 0em
-  \expandafter \mpr@makelist #2\mpr@to \mpr@flat
-  \if@premisse \mpr@rev \mpr@flat \mpr@to \@rev \else \let \@rev \mpr@flat \fi
-  \def \\##1{%
-     \def \@test {##1}\ifx \@test \empty
-        \mpr@htovlist
-        \mpr@tmpdim 0em %%% last bug fix not extensively checked
-     \else
-      \setbox0 \hbox{$\displaystyle {##1}$}\relax
-      \advance \mpr@tmpdim by \wd0
-      %\mpr@tmpdim 1.02\mpr@tmpdim
-      \ifnum \mpr@tmpdim < \hsize
-         \ifnum \wd\mpr@hlist > 0
-           \if@premisse
-             \setbox \mpr@hlist 
-                \hbox {\unhbox0 \hskip \mpr@sep \unhbox \mpr@hlist}%
-           \else
-             \setbox \mpr@hlist
-                \hbox {\unhbox \mpr@hlist  \hskip \mpr@sep \unhbox0}%
-           \fi
-         \else 
-         \setbox \mpr@hlist \hbox {\unhbox0}%
-         \fi
-      \else
-         \ifnum \wd \mpr@hlist > 0
-            \mpr@htovlist 
-            \mpr@tmpdim \wd0
-         \fi
-         \setbox \mpr@hlist \hbox {\unhbox0}%
-      \fi
-      \advance \mpr@tmpdim by \mpr@sep
-   \fi
-   }%
-   \@rev
-   \mpr@htovlist
-   \ifmpr@center \hskip \wd\mpr@vlist\fi \box \mpr@vlist
-   \fi
-   \egroup
-}
-
-%%% INFERENCE RULES
-
-\@ifundefined{@@over}{%
-    \let\@@over\over % fallback if amsmath is not loaded
-    \let\@@overwithdelims\overwithdelims
-    \let\@@atop\atop \let\@@atopwithdelims\atopwithdelims
-    \let\@@above\above \let\@@abovewithdelims\abovewithdelims
-  }{}
-
-
-\def \mpr@@fraction #1#2{\hbox {\advance \hsize by -0.5em
-    $\displaystyle {#1\@@over #2}$}}
-\let \mpr@fraction \mpr@@fraction
-\def \mpr@@reduce #1#2{\hbox
-    {$\lower 0.01pt \mpr@@fraction {#1}{#2}\mkern -15mu\rightarrow$}}
-\def \mpr@@rewrite #1#2#3{\hbox
-    {$\lower 0.01pt \mpr@@fraction {#2}{#3}\mkern -8mu#1$}}
-\def \mpr@infercenter #1{\vcenter {\mpr@hovbox{T}{#1}}}
-
-\def \mpr@empty {}
-\def \mpr@inferrule
-  {\bgroup
-     \ifnum \linewidth<\hsize \hsize \linewidth\fi
-     \mpr@rulelineskip
-     \let \and \qquad
-     \let \hva \mpr@hva
-     \let \@rulename \mpr@empty
-     \let \@rule@options \mpr@empty
-     \mpr@inferrule@}
-\newcommand {\mpr@inferrule@}[3][]
-  {\everymath={\displaystyle}%       
-   \def \@test {#2}\ifx \empty \@test
-      \setbox0 \hbox {$\vcenter {\mpr@hovbox{B}{#3}}$}%
-   \else 
-   \def \@test {#3}\ifx \empty \@test
-      \setbox0 \hbox {$\vcenter {\mpr@hovbox{T}{#2}}$}%
-   \else
-   \setbox0 \mpr@fraction {\mpr@hovbox{T}{#2}}{\mpr@hovbox{B}{#3}}%
-   \fi \fi
-   \def \@test {#1}\ifx \@test\empty \box0
-   \else \vbox 
-%%% Suggestion de Francois pour les etiquettes longues
-%%%   {\hbox to \wd0 {\RefTirName {#1}\hfil}\box0}\fi
-      {\hbox {\RefTirName {#1}}\box0}\fi
-   \egroup}
-
-\def \mpr@vdotfil #1{\vbox to #1{\leaders \hbox{$\cdot$} \vfil}}
-
-% They are two forms
-% \inferrule [label]{[premisses}{conclusions}
-% or
-% \inferrule* [options]{[premisses}{conclusions}
-%
-% Premisses and conclusions are lists of elements separated by \\
-% Each \\ produces a break, attempting horizontal breaks if possible, 
-% and  vertical breaks if needed. 
-% 
-% An empty element obtained by \\\\ produces a vertical break in all cases. 
-%
-% The former rule is aligned on the fraction bar. 
-% The optional label appears on top of the rule
-% The second form to be used in a derivation tree is aligned on the last
-% line of its conclusion
-% 
-% The second form can be parameterized, using the key=val interface. The
-% folloiwng keys are recognized:
-%       
-%  width                set the width of the rule to val
-%  narrower             set the width of the rule to val\hsize
-%  before               execute val at the beginning/left
-%  lab                  put a label [Val] on top of the rule
-%  lskip                add negative skip on the right
-%  left                 put a left label [Val]
-%  Left                 put a left label [Val],  ignoring its width 
-%  right                put a right label [Val]
-%  Right                put a right label [Val], ignoring its width
-%  leftskip             skip negative space on the left-hand side
-%  rightskip            skip negative space on the right-hand side
-%  vdots                lift the rule by val and fill vertical space with dots
-%  after                execute val at the end/right
-%  
-%  Note that most options must come in this order to avoid strange
-%  typesetting (in particular  leftskip must preceed left and Left and
-%  rightskip must follow Right or right; vdots must come last 
-%  or be only followed by rightskip. 
-%  
-
-\define@key {mprset}{flushleft}[]{\mpr@centerfalse}
-\define@key {mprset}{center}[]{\mpr@centertrue}
-\def \mprset #1{\setkeys{mprset}{#1}}
-
-\newbox \mpr@right
-\define@key {mpr}{flushleft}[]{\mpr@centerfalse}
-\define@key {mpr}{center}[]{\mpr@centertrue}
-\define@key {mpr}{left}{\setbox0 \hbox {$\TirName {#1}\;$}\relax
-     \advance \hsize by -\wd0\box0}
-\define@key {mpr}{width}{\hsize #1}
-\define@key {mpr}{sep}{\def\mpr@sep{#1}}
-\define@key {mpr}{before}{#1}
-\define@key {mpr}{lab}{\let \RefTirName \TirName \def \mpr@rulename {#1}}
-\define@key {mpr}{Lab}{\let \RefTirName \TirName \def \mpr@rulename {#1}}
-\define@key {mpr}{narrower}{\hsize #1\hsize}
-\define@key {mpr}{leftskip}{\hskip -#1}
-\define@key {mpr}{reduce}[]{\let \mpr@fraction \mpr@@reduce}
-\define@key {mpr}{rightskip}
-  {\setbox \mpr@right \hbox {\unhbox \mpr@right \hskip -#1}}
-\define@key {mpr}{LEFT}{\setbox0 \hbox {$#1$}\relax
-     \advance \hsize by -\wd0\box0}
-\define@key {mpr}{left}{\setbox0 \hbox {$\TirName {#1}\;$}\relax
-     \advance \hsize by -\wd0\box0}
-\define@key {mpr}{Left}{\llap{$\TirName {#1}\;$}}
-\define@key {mpr}{right}
-  {\setbox0 \hbox {$\;\TirName {#1}$}\relax \advance \hsize by -\wd0
-   \setbox \mpr@right \hbox {\unhbox \mpr@right \unhbox0}}
-\define@key {mpr}{RIGHT}
-  {\setbox0 \hbox {$#1$}\relax \advance \hsize by -\wd0
-   \setbox \mpr@right \hbox {\unhbox \mpr@right \unhbox0}}
-\define@key {mpr}{Right}
-  {\setbox \mpr@right \hbox {\unhbox \mpr@right \rlap {$\;\TirName {#1}$}}}
-\define@key {mpr}{vdots}{\def \mpr@vdots {\@@atop \mpr@vdotfil{#1}}}
-\define@key {mpr}{after}{\edef \mpr@after {\mpr@after #1}}
-
-\newdimen \rule@dimen
-\newcommand \mpr@inferstar@ [3][]{\setbox0
-  \hbox {\let \mpr@rulename \mpr@empty \let \mpr@vdots \relax
-         \setbox \mpr@right \hbox{}%
-         $\setkeys{mpr}{#1}%
-          \ifx \mpr@rulename \mpr@empty \mpr@inferrule {#2}{#3}\else
-          \mpr@inferrule [{\mpr@rulename}]{#2}{#3}\fi
-          \box \mpr@right \mpr@vdots$}
-  \setbox1 \hbox {\strut}
-  \rule@dimen \dp0 \advance \rule@dimen by -\dp1
-  \raise \rule@dimen \box0}
-
-\def \mpr@infer {\@ifnextchar *{\mpr@inferstar}{\mpr@inferrule}}
-\newcommand \mpr@err@skipargs[3][]{}
-\def \mpr@inferstar*{\ifmmode 
-    \let \@do \mpr@inferstar@
-  \else 
-    \let \@do \mpr@err@skipargs
-    \PackageError {mathpartir}
-      {\string\inferrule* can only be used in math mode}{}%
-  \fi \@do}
-
-
-%%% Exports
-
-% Envirnonment mathpar
-
-\let \inferrule \mpr@infer
-
-% make a short name \infer is not already defined
-\@ifundefined {infer}{\let \infer \mpr@infer}{}
-
-\def \tir@name #1{\hbox {\small \sc #1}}
-\let \TirName \tir@name
-\let \RefTirName \tir@name
-
-%%% Other Exports
-
-% \let \listcons \mpr@cons
-% \let \listsnoc \mpr@snoc
-% \let \listhead \mpr@head
-% \let \listmake \mpr@makelist
-
-
-
-
-\endinput
diff -r 8c5b8d7999bd -r dc51115fa4aa src/Doc/ROOT
--- a/src/Doc/ROOT	Fri Sep 11 13:54:22 2020 +0200
+++ b/src/Doc/ROOT	Fri Sep 11 14:04:16 2020 +0200
@@ -117,7 +117,6 @@
     "build"
     "conclusion.tex"
     "intro.tex"
-    "mathpartir.sty"
     "root.tex"
     "style.sty"
 
@@ -258,7 +257,6 @@
     "pdfsetup.sty"
   document_files
     "build"
-    "mathpartir.sty"
     "root.bib"
     "root.tex"
 
@@ -360,7 +358,6 @@
     "bang.pdf"
     "build"
     "intro-isabelle.tex"
-    "mathpartir.sty"
     "prelude.tex"
     "root.bib"
     "root.tex"
diff -r 8c5b8d7999bd -r dc51115fa4aa src/Doc/Sugar/document/mathpartir.sty
--- a/src/Doc/Sugar/document/mathpartir.sty	Fri Sep 11 13:54:22 2020 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,388 +0,0 @@
-%  Mathpartir --- Math Paragraph for Typesetting Inference Rules
-%
-%  Copyright (C) 2001, 2002, 2003 Didier Rémy
-%
-%  Author         : Didier Remy 
-%  Version        : 1.1.1
-%  Bug Reports    : to author
-%  Web Site       : http://pauillac.inria.fr/~remy/latex/
-% 
-%  WhizzyTeX is free software; you can redistribute it and/or modify
-%  it under the terms of the GNU General Public License as published by
-%  the Free Software Foundation; either version 2, or (at your option)
-%  any later version.
-%  
-%  Mathpartir is distributed in the hope that it will be useful,
-%  but WITHOUT ANY WARRANTY; without even the implied warranty of
-%  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
-%  GNU General Public License for more details 
-%  (http://pauillac.inria.fr/~remy/license/GPL).
-%
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-%  File mathpartir.sty (LaTeX macros)
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-
-\NeedsTeXFormat{LaTeX2e}
-\ProvidesPackage{mathpartir}
-    [2003/07/10 version 1.1.1 Math Paragraph for Typesetting Inference Rules]
-
-%%
-
-%% Identification
-%% Preliminary declarations
-
-\RequirePackage {keyval}
-
-%% Options
-%% More declarations
-
-%% PART I: Typesetting maths in paragraphe mode
-
-\newdimen \mpr@tmpdim
-
-% To ensure hevea \hva compatibility, \hva should expands to nothing 
-% in mathpar or in inferrule
-\let \mpr@hva \empty
-
-%% normal paragraph parametters, should rather be taken dynamically
-\def \mpr@savepar {%
-  \edef \MathparNormalpar
-     {\noexpand \lineskiplimit \the\lineskiplimit
-      \noexpand \lineskip \the\lineskip}%
-  }
-
-\def \mpr@rulelineskip {\lineskiplimit=0.3em\lineskip=0.2em plus 0.1em}
-\def \mpr@lesslineskip {\lineskiplimit=0.6em\lineskip=0.5em plus 0.2em}
-\def \mpr@lineskip  {\lineskiplimit=1.2em\lineskip=1.2em plus 0.2em}
-\let \MathparLineskip \mpr@lineskip
-\def \mpr@paroptions {\MathparLineskip}
-\let \mpr@prebindings \relax
-
-\newskip \mpr@andskip \mpr@andskip 2em plus 0.5fil minus 0.5em
-
-\def \mpr@goodbreakand
-   {\hskip -\mpr@andskip  \penalty -1000\hskip \mpr@andskip}
-\def \mpr@and {\hskip \mpr@andskip}
-\def \mpr@andcr {\penalty 50\mpr@and}
-\def \mpr@cr {\penalty -10000\mpr@and}
-\def \mpr@eqno #1{\mpr@andcr #1\hskip 0em plus -1fil \penalty 10}
-
-\def \mpr@bindings {%
-  \let \and \mpr@andcr
-  \let \par \mpr@andcr
-  \let \\\mpr@cr
-  \let \eqno \mpr@eqno
-  \let \hva \mpr@hva
-  } 
-\let \MathparBindings \mpr@bindings
-
-% \@ifundefined {ignorespacesafterend}
-%    {\def \ignorespacesafterend {\aftergroup \ignorespaces}
-
-\newenvironment{mathpar}[1][]
-  {$$\mpr@savepar \parskip 0em \hsize \linewidth \centering
-     \vbox \bgroup \mpr@prebindings \mpr@paroptions #1\ifmmode $\else
-     \noindent $\displaystyle\fi
-     \MathparBindings}
-  {\unskip \ifmmode $\fi\egroup $$\ignorespacesafterend}
-
-% \def \math@mathpar #1{\setbox0 \hbox {$\displaystyle #1$}\ifnum
-%     \wd0 < \hsize  $$\box0$$\else \bmathpar #1\emathpar \fi}
-
-%%% HOV BOXES
-
-\def \mathvbox@ #1{\hbox \bgroup \mpr@normallineskip 
-  \vbox \bgroup \tabskip 0em \let \\ \cr
-  \halign \bgroup \hfil $##$\hfil\cr #1\crcr \egroup \egroup
-  \egroup}
-
-\def \mathhvbox@ #1{\setbox0 \hbox {\let \\\qquad $#1$}\ifnum \wd0 < \hsize
-      \box0\else \mathvbox {#1}\fi}
-
-
-%% Part II -- operations on lists
-
-\newtoks \mpr@lista
-\newtoks \mpr@listb
-
-\long \def\mpr@cons #1\mpr@to#2{\mpr@lista {\\{#1}}\mpr@listb \expandafter
-{#2}\edef #2{\the \mpr@lista \the \mpr@listb}}
-
-\long \def\mpr@snoc #1\mpr@to#2{\mpr@lista {\\{#1}}\mpr@listb \expandafter
-{#2}\edef #2{\the \mpr@listb\the\mpr@lista}}
-
-\long \def \mpr@concat#1=#2\mpr@to#3{\mpr@lista \expandafter {#2}\mpr@listb
-\expandafter {#3}\edef #1{\the \mpr@listb\the\mpr@lista}}
-
-\def \mpr@head #1\mpr@to #2{\expandafter \mpr@head@ #1\mpr@head@ #1#2}
-\long \def \mpr@head@ #1#2\mpr@head@ #3#4{\def #4{#1}\def#3{#2}}
-
-\def \mpr@flatten #1\mpr@to #2{\expandafter \mpr@flatten@ #1\mpr@flatten@ #1#2}
-\long \def \mpr@flatten@ \\#1\\#2\mpr@flatten@ #3#4{\def #4{#1}\def #3{\\#2}}
-
-\def \mpr@makelist #1\mpr@to #2{\def \mpr@all {#1}%
-   \mpr@lista {\\}\mpr@listb \expandafter {\mpr@all}\edef \mpr@all {\the
-   \mpr@lista \the \mpr@listb \the \mpr@lista}\let #2\empty 
-   \def \mpr@stripof ##1##2\mpr@stripend{\def \mpr@stripped{##2}}\loop
-     \mpr@flatten \mpr@all \mpr@to \mpr@one
-     \expandafter \mpr@snoc \mpr@one \mpr@to #2\expandafter \mpr@stripof
-     \mpr@all \mpr@stripend  
-     \ifx \mpr@stripped \empty \let \mpr@isempty 0\else \let \mpr@isempty 1\fi
-     \ifx 1\mpr@isempty
-   \repeat
-}
-
-%% Part III -- Type inference rules
-
-\def \mpr@rev #1\mpr@to #2{\let \mpr@tmp \empty
-   \def \\##1{\mpr@cons ##1\mpr@to \mpr@tmp}#1\let #2\mpr@tmp}
-
-\newif \if@premisse
-\newbox \mpr@hlist
-\newbox \mpr@vlist
-\newif \ifmpr@center \mpr@centertrue
-\def \mpr@htovlist {%
-   \setbox \mpr@hlist
-      \hbox {\strut
-             \ifmpr@center \hskip -0.5\wd\mpr@hlist\fi
-             \unhbox \mpr@hlist}%
-   \setbox \mpr@vlist
-      \vbox {\if@premisse  \box \mpr@hlist \unvbox \mpr@vlist
-             \else \unvbox \mpr@vlist \box \mpr@hlist
-             \fi}%
-}
-% OLD version
-% \def \mpr@htovlist {%
-%    \setbox \mpr@hlist
-%       \hbox {\strut \hskip -0.5\wd\mpr@hlist \unhbox \mpr@hlist}%
-%    \setbox \mpr@vlist
-%       \vbox {\if@premisse  \box \mpr@hlist \unvbox \mpr@vlist
-%              \else \unvbox \mpr@vlist \box \mpr@hlist
-%              \fi}%
-% }
-
-\def \mpr@sep{2em}
-\def \mpr@blank { }
-\def \mpr@hovbox #1#2{\hbox
-  \bgroup
-  \ifx #1T\@premissetrue
-  \else \ifx #1B\@premissefalse
-  \else
-     \PackageError{mathpartir}
-       {Premisse orientation should either be P or B}
-       {Fatal error in Package}%
-  \fi \fi
-  \def \@test {#2}\ifx \@test \mpr@blank\else
-  \setbox \mpr@hlist \hbox {}%
-  \setbox \mpr@vlist \vbox {}%
-  \if@premisse \let \snoc \mpr@cons \else \let \snoc \mpr@snoc \fi
-  \let \@hvlist \empty \let \@rev \empty
-  \mpr@tmpdim 0em
-  \expandafter \mpr@makelist #2\mpr@to \mpr@flat
-  \if@premisse \mpr@rev \mpr@flat \mpr@to \@rev \else \let \@rev \mpr@flat \fi
-  \def \\##1{%
-     \def \@test {##1}\ifx \@test \empty
-        \mpr@htovlist
-        \mpr@tmpdim 0em %%% last bug fix not extensively checked
-     \else
-      \setbox0 \hbox{$\displaystyle {##1}$}\relax
-      \advance \mpr@tmpdim by \wd0
-      %\mpr@tmpdim 1.02\mpr@tmpdim
-      \ifnum \mpr@tmpdim < \hsize
-         \ifnum \wd\mpr@hlist > 0
-           \if@premisse
-             \setbox \mpr@hlist 
-                \hbox {\unhbox0 \hskip \mpr@sep \unhbox \mpr@hlist}%
-           \else
-             \setbox \mpr@hlist
-                \hbox {\unhbox \mpr@hlist  \hskip \mpr@sep \unhbox0}%
-           \fi
-         \else 
-         \setbox \mpr@hlist \hbox {\unhbox0}%
-         \fi
-      \else
-         \ifnum \wd \mpr@hlist > 0
-            \mpr@htovlist 
-            \mpr@tmpdim \wd0
-         \fi
-         \setbox \mpr@hlist \hbox {\unhbox0}%
-      \fi
-      \advance \mpr@tmpdim by \mpr@sep
-   \fi
-   }%
-   \@rev
-   \mpr@htovlist
-   \ifmpr@center \hskip \wd\mpr@vlist\fi \box \mpr@vlist
-   \fi
-   \egroup
-}
-
-%%% INFERENCE RULES
-
-\@ifundefined{@@over}{%
-    \let\@@over\over % fallback if amsmath is not loaded
-    \let\@@overwithdelims\overwithdelims
-    \let\@@atop\atop \let\@@atopwithdelims\atopwithdelims
-    \let\@@above\above \let\@@abovewithdelims\abovewithdelims
-  }{}
-
-
-\def \mpr@@fraction #1#2{\hbox {\advance \hsize by -0.5em
-    $\displaystyle {#1\@@over #2}$}}
-\let \mpr@fraction \mpr@@fraction
-\def \mpr@@reduce #1#2{\hbox
-    {$\lower 0.01pt \mpr@@fraction {#1}{#2}\mkern -15mu\rightarrow$}}
-\def \mpr@@rewrite #1#2#3{\hbox
-    {$\lower 0.01pt \mpr@@fraction {#2}{#3}\mkern -8mu#1$}}
-\def \mpr@infercenter #1{\vcenter {\mpr@hovbox{T}{#1}}}
-
-\def \mpr@empty {}
-\def \mpr@inferrule
-  {\bgroup
-     \ifnum \linewidth<\hsize \hsize \linewidth\fi
-     \mpr@rulelineskip
-     \let \and \qquad
-     \let \hva \mpr@hva
-     \let \@rulename \mpr@empty
-     \let \@rule@options \mpr@empty
-     \mpr@inferrule@}
-\newcommand {\mpr@inferrule@}[3][]
-  {\everymath={\displaystyle}%       
-   \def \@test {#2}\ifx \empty \@test
-      \setbox0 \hbox {$\vcenter {\mpr@hovbox{B}{#3}}$}%
-   \else 
-   \def \@test {#3}\ifx \empty \@test
-      \setbox0 \hbox {$\vcenter {\mpr@hovbox{T}{#2}}$}%
-   \else
-   \setbox0 \mpr@fraction {\mpr@hovbox{T}{#2}}{\mpr@hovbox{B}{#3}}%
-   \fi \fi
-   \def \@test {#1}\ifx \@test\empty \box0
-   \else \vbox 
-%%% Suggestion de Francois pour les etiquettes longues
-%%%   {\hbox to \wd0 {\RefTirName {#1}\hfil}\box0}\fi
-      {\hbox {\RefTirName {#1}}\box0}\fi
-   \egroup}
-
-\def \mpr@vdotfil #1{\vbox to #1{\leaders \hbox{$\cdot$} \vfil}}
-
-% They are two forms
-% \inferrule [label]{[premisses}{conclusions}
-% or
-% \inferrule* [options]{[premisses}{conclusions}
-%
-% Premisses and conclusions are lists of elements separated by \\
-% Each \\ produces a break, attempting horizontal breaks if possible, 
-% and  vertical breaks if needed. 
-% 
-% An empty element obtained by \\\\ produces a vertical break in all cases. 
-%
-% The former rule is aligned on the fraction bar. 
-% The optional label appears on top of the rule
-% The second form to be used in a derivation tree is aligned on the last
-% line of its conclusion
-% 
-% The second form can be parameterized, using the key=val interface. The
-% folloiwng keys are recognized:
-%       
-%  width                set the width of the rule to val
-%  narrower             set the width of the rule to val\hsize
-%  before               execute val at the beginning/left
-%  lab                  put a label [Val] on top of the rule
-%  lskip                add negative skip on the right
-%  left                 put a left label [Val]
-%  Left                 put a left label [Val],  ignoring its width 
-%  right                put a right label [Val]
-%  Right                put a right label [Val], ignoring its width
-%  leftskip             skip negative space on the left-hand side
-%  rightskip            skip negative space on the right-hand side
-%  vdots                lift the rule by val and fill vertical space with dots
-%  after                execute val at the end/right
-%  
-%  Note that most options must come in this order to avoid strange
-%  typesetting (in particular  leftskip must preceed left and Left and
-%  rightskip must follow Right or right; vdots must come last 
-%  or be only followed by rightskip. 
-%  
-
-\define@key {mprset}{flushleft}[]{\mpr@centerfalse}
-\define@key {mprset}{center}[]{\mpr@centertrue}
-\def \mprset #1{\setkeys{mprset}{#1}}
-
-\newbox \mpr@right
-\define@key {mpr}{flushleft}[]{\mpr@centerfalse}
-\define@key {mpr}{center}[]{\mpr@centertrue}
-\define@key {mpr}{left}{\setbox0 \hbox {$\TirName {#1}\;$}\relax
-     \advance \hsize by -\wd0\box0}
-\define@key {mpr}{width}{\hsize #1}
-\define@key {mpr}{sep}{\def\mpr@sep{#1}}
-\define@key {mpr}{before}{#1}
-\define@key {mpr}{lab}{\let \RefTirName \TirName \def \mpr@rulename {#1}}
-\define@key {mpr}{Lab}{\let \RefTirName \TirName \def \mpr@rulename {#1}}
-\define@key {mpr}{narrower}{\hsize #1\hsize}
-\define@key {mpr}{leftskip}{\hskip -#1}
-\define@key {mpr}{reduce}[]{\let \mpr@fraction \mpr@@reduce}
-\define@key {mpr}{rightskip}
-  {\setbox \mpr@right \hbox {\unhbox \mpr@right \hskip -#1}}
-\define@key {mpr}{LEFT}{\setbox0 \hbox {$#1$}\relax
-     \advance \hsize by -\wd0\box0}
-\define@key {mpr}{left}{\setbox0 \hbox {$\TirName {#1}\;$}\relax
-     \advance \hsize by -\wd0\box0}
-\define@key {mpr}{Left}{\llap{$\TirName {#1}\;$}}
-\define@key {mpr}{right}
-  {\setbox0 \hbox {$\;\TirName {#1}$}\relax \advance \hsize by -\wd0
-   \setbox \mpr@right \hbox {\unhbox \mpr@right \unhbox0}}
-\define@key {mpr}{RIGHT}
-  {\setbox0 \hbox {$#1$}\relax \advance \hsize by -\wd0
-   \setbox \mpr@right \hbox {\unhbox \mpr@right \unhbox0}}
-\define@key {mpr}{Right}
-  {\setbox \mpr@right \hbox {\unhbox \mpr@right \rlap {$\;\TirName {#1}$}}}
-\define@key {mpr}{vdots}{\def \mpr@vdots {\@@atop \mpr@vdotfil{#1}}}
-\define@key {mpr}{after}{\edef \mpr@after {\mpr@after #1}}
-
-\newdimen \rule@dimen
-\newcommand \mpr@inferstar@ [3][]{\setbox0
-  \hbox {\let \mpr@rulename \mpr@empty \let \mpr@vdots \relax
-         \setbox \mpr@right \hbox{}%
-         $\setkeys{mpr}{#1}%
-          \ifx \mpr@rulename \mpr@empty \mpr@inferrule {#2}{#3}\else
-          \mpr@inferrule [{\mpr@rulename}]{#2}{#3}\fi
-          \box \mpr@right \mpr@vdots$}
-  \setbox1 \hbox {\strut}
-  \rule@dimen \dp0 \advance \rule@dimen by -\dp1
-  \raise \rule@dimen \box0}
-
-\def \mpr@infer {\@ifnextchar *{\mpr@inferstar}{\mpr@inferrule}}
-\newcommand \mpr@err@skipargs[3][]{}
-\def \mpr@inferstar*{\ifmmode 
-    \let \@do \mpr@inferstar@
-  \else 
-    \let \@do \mpr@err@skipargs
-    \PackageError {mathpartir}
-      {\string\inferrule* can only be used in math mode}{}%
-  \fi \@do}
-
-
-%%% Exports
-
-% Envirnonment mathpar
-
-\let \inferrule \mpr@infer
-
-% make a short name \infer is not already defined
-\@ifundefined {infer}{\let \infer \mpr@infer}{}
-
-\def \tir@name #1{\hbox {\small \sc #1}}
-\let \TirName \tir@name
-\let \RefTirName \tir@name
-
-%%% Other Exports
-
-% \let \listcons \mpr@cons
-% \let \listsnoc \mpr@snoc
-% \let \listhead \mpr@head
-% \let \listmake \mpr@makelist
-
-
-
-
-\endinput