1.1 --- a/src/Doc/Classes/document/build	Fri Dec 07 17:00:40 2012 +0100
     1.2 +++ b/src/Doc/Classes/document/build	Fri Dec 07 18:05:24 2012 +0100
     1.3 @@ -10,7 +10,6 @@
     1.4  cp "$ISABELLE_HOME/src/Doc/iman.sty" .
     1.5  cp "$ISABELLE_HOME/src/Doc/extra.sty" .
     1.6  cp "$ISABELLE_HOME/src/Doc/isar.sty" .
     1.7 -cp "$ISABELLE_HOME/src/Doc/proof.sty" .
     1.8  cp "$ISABELLE_HOME/src/Doc/manual.bib" .
     1.9  
    1.10  "$ISABELLE_HOME/src/Doc/prepare_document" "$FORMAT"

     2.1 --- a/src/Doc/Classes/document/root.tex	Fri Dec 07 17:00:40 2012 +0100
     2.2 +++ b/src/Doc/Classes/document/root.tex	Fri Dec 07 18:05:24 2012 +0100
     2.3 @@ -1,6 +1,6 @@
     2.4  \documentclass[12pt,a4paper,fleqn]{article}
     2.5  \usepackage{latexsym,graphicx}
     2.6 -\usepackage{iman,extra,isar,proof}
     2.7 +\usepackage{iman,extra,isar}
     2.8  \usepackage{isabelle,isabellesym}
     2.9  \usepackage{style}
    2.10  \usepackage{pdfsetup}

     3.1 --- a/src/Doc/Codegen/document/build	Fri Dec 07 17:00:40 2012 +0100
     3.2 +++ b/src/Doc/Codegen/document/build	Fri Dec 07 18:05:24 2012 +0100
     3.3 @@ -10,7 +10,6 @@
     3.4  cp "$ISABELLE_HOME/src/Doc/iman.sty" .
     3.5  cp "$ISABELLE_HOME/src/Doc/extra.sty" .
     3.6  cp "$ISABELLE_HOME/src/Doc/isar.sty" .
     3.7 -cp "$ISABELLE_HOME/src/Doc/proof.sty" .
     3.8  cp "$ISABELLE_HOME/src/Doc/manual.bib" .
     3.9  
    3.10  for NAME in architecture adapt

     4.1 --- a/src/Doc/Codegen/document/root.tex	Fri Dec 07 17:00:40 2012 +0100
     4.2 +++ b/src/Doc/Codegen/document/root.tex	Fri Dec 07 18:05:24 2012 +0100
     4.3 @@ -2,7 +2,7 @@
     4.4  \documentclass[12pt,a4paper,fleqn]{article}
     4.5  \usepackage{latexsym,graphicx}
     4.6  \usepackage{multirow}
     4.7 -\usepackage{iman,extra,isar,proof}
     4.8 +\usepackage{iman,extra,isar}
     4.9  \usepackage{isabelle,isabellesym}
    4.10  \usepackage{style}
    4.11  \usepackage{pdfsetup}

     5.1 --- a/src/Doc/HOL/document/build	Fri Dec 07 17:00:40 2012 +0100
     5.2 +++ b/src/Doc/HOL/document/build	Fri Dec 07 18:05:24 2012 +0100
     5.3 @@ -10,7 +10,6 @@
     5.4  cp "$ISABELLE_HOME/src/Doc/iman.sty" .
     5.5  cp "$ISABELLE_HOME/src/Doc/extra.sty" .
     5.6  cp "$ISABELLE_HOME/src/Doc/ttbox.sty" .
     5.7 -cp "$ISABELLE_HOME/src/Doc/proof.sty" .
     5.8  cp "$ISABELLE_HOME/src/Doc/manual.bib" .
     5.9  cp "$ISABELLE_HOME/src/Doc/Logics/document/syntax.tex" .
    5.10  

     6.1 --- a/src/Doc/Intro/document/build	Fri Dec 07 17:00:40 2012 +0100
     6.2 +++ b/src/Doc/Intro/document/build	Fri Dec 07 18:05:24 2012 +0100
     6.3 @@ -10,7 +10,6 @@
     6.4  cp "$ISABELLE_HOME/src/Doc/iman.sty" .
     6.5  cp "$ISABELLE_HOME/src/Doc/extra.sty" .
     6.6  cp "$ISABELLE_HOME/src/Doc/ttbox.sty" .
     6.7 -cp "$ISABELLE_HOME/src/Doc/proof.sty" .
     6.8  cp "$ISABELLE_HOME/src/Doc/manual.bib" .
     6.9  
    6.10  "$ISABELLE_HOME/src/Doc/prepare_document" "$FORMAT"

     7.1 --- a/src/Doc/IsarImplementation/document/build	Fri Dec 07 17:00:40 2012 +0100
     7.2 +++ b/src/Doc/IsarImplementation/document/build	Fri Dec 07 18:05:24 2012 +0100
     7.3 @@ -10,7 +10,6 @@
     7.4  cp "$ISABELLE_HOME/src/Doc/iman.sty" .
     7.5  cp "$ISABELLE_HOME/src/Doc/extra.sty" .
     7.6  cp "$ISABELLE_HOME/src/Doc/isar.sty" .
     7.7 -cp "$ISABELLE_HOME/src/Doc/proof.sty" .
     7.8  cp "$ISABELLE_HOME/src/Doc/ttbox.sty" .
     7.9  cp "$ISABELLE_HOME/src/Doc/underscore.sty" .
    7.10  cp "$ISABELLE_HOME/src/Doc/manual.bib" .

     8.1 --- a/src/Doc/Logics/document/build	Fri Dec 07 17:00:40 2012 +0100
     8.2 +++ b/src/Doc/Logics/document/build	Fri Dec 07 18:05:24 2012 +0100
     8.3 @@ -10,7 +10,6 @@
     8.4  cp "$ISABELLE_HOME/src/Doc/iman.sty" .
     8.5  cp "$ISABELLE_HOME/src/Doc/extra.sty" .
     8.6  cp "$ISABELLE_HOME/src/Doc/ttbox.sty" .
     8.7 -cp "$ISABELLE_HOME/src/Doc/proof.sty" .
     8.8  cp "$ISABELLE_HOME/src/Doc/manual.bib" .
     8.9  
    8.10  "$ISABELLE_HOME/src/Doc/prepare_document" "$FORMAT"

     9.1 --- a/src/Doc/ROOT	Fri Dec 07 17:00:40 2012 +0100
     9.2 +++ b/src/Doc/ROOT	Fri Dec 07 18:05:24 2012 +0100
     9.3 @@ -8,7 +8,6 @@
     9.4      "../iman.sty"
     9.5      "../extra.sty"
     9.6      "../isar.sty"
     9.7 -    "../proof.sty"
     9.8      "../manual.bib"
     9.9      "document/build"
    9.10      "document/root.tex"
    9.11 @@ -31,7 +30,6 @@
    9.12      "../iman.sty"
    9.13      "../extra.sty"
    9.14      "../isar.sty"
    9.15 -    "../proof.sty"
    9.16      "../manual.bib"
    9.17      "document/adapt.tex"
    9.18      "document/architecture.tex"
    9.19 @@ -65,7 +63,6 @@
    9.20      "../iman.sty"
    9.21      "../extra.sty"
    9.22      "../ttbox.sty"
    9.23 -    "../proof.sty"
    9.24      "../manual.bib"
    9.25      "document/build"
    9.26      "document/root.tex"
    9.27 @@ -89,7 +86,6 @@
    9.28      "../iman.sty"
    9.29      "../extra.sty"
    9.30      "../isar.sty"
    9.31 -    "../proof.sty"
    9.32      "../ttbox.sty"
    9.33      "../underscore.sty"
    9.34      "../manual.bib"
    9.35 @@ -167,7 +163,6 @@
    9.36      "../iman.sty"
    9.37      "../extra.sty"
    9.38      "../ttbox.sty"
    9.39 -    "../proof.sty"
    9.40      "../manual.bib"
    9.41      "document/build"
    9.42      "document/root.tex"
    9.43 @@ -181,7 +176,6 @@
    9.44      "../iman.sty"
    9.45      "../extra.sty"
    9.46      "../ttbox.sty"
    9.47 -    "../proof.sty"
    9.48      "../manual.bib"
    9.49      "../Logics/document/syntax.tex"
    9.50      "document/build"
    9.51 @@ -201,7 +195,6 @@
    9.52      "../pdfsetup.sty"
    9.53      "../isar.sty"
    9.54      "../ttbox.sty"
    9.55 -    "../proof.sty"
    9.56      "../manual.bib"
    9.57      "../Logics/document/syntax.tex"
    9.58      "document/build"
    9.59 @@ -258,7 +251,6 @@
    9.60      "../iman.sty"
    9.61      "../extra.sty"
    9.62      "../ttbox.sty"
    9.63 -    "../proof.sty"
    9.64      "../manual.bib"
    9.65      "document/build"
    9.66      "document/root.tex"
    9.67 @@ -363,7 +355,6 @@
    9.68      "ToyList/ToyList1"
    9.69      "ToyList/ToyList2"
    9.70      "../pdfsetup.sty"
    9.71 -    "../proof.sty"
    9.72      "../ttbox.sty"
    9.73      "../manual.bib"
    9.74      "document/advanced0.tex"

    10.1 --- a/src/Doc/Ref/document/build	Fri Dec 07 17:00:40 2012 +0100
    10.2 +++ b/src/Doc/Ref/document/build	Fri Dec 07 18:05:24 2012 +0100
    10.3 @@ -10,7 +10,6 @@
    10.4  cp "$ISABELLE_HOME/src/Doc/iman.sty" .
    10.5  cp "$ISABELLE_HOME/src/Doc/extra.sty" .
    10.6  cp "$ISABELLE_HOME/src/Doc/ttbox.sty" .
    10.7 -cp "$ISABELLE_HOME/src/Doc/proof.sty" .
    10.8  cp "$ISABELLE_HOME/src/Doc/manual.bib" .
    10.9  
   10.10  "$ISABELLE_HOME/src/Doc/prepare_document" "$FORMAT"

    11.1 --- a/src/Doc/Ref/document/root.tex	Fri Dec 07 17:00:40 2012 +0100
    11.2 +++ b/src/Doc/Ref/document/root.tex	Fri Dec 07 18:05:24 2012 +0100
    11.3 @@ -1,5 +1,5 @@
    11.4  \documentclass[12pt,a4paper]{report}
    11.5 -\usepackage{graphicx,iman,extra,ttbox,proof,pdfsetup}
    11.6 +\usepackage{graphicx,iman,extra,ttbox,pdfsetup}
    11.7  
    11.8  \title{\includegraphics[scale=0.5]{isabelle} \\[4ex] Old Isabelle Reference Manual}
    11.9  

    12.1 --- a/src/Doc/Tutorial/document/build	Fri Dec 07 17:00:40 2012 +0100
    12.2 +++ b/src/Doc/Tutorial/document/build	Fri Dec 07 18:05:24 2012 +0100
    12.3 @@ -7,7 +7,6 @@
    12.4  
    12.5  "$ISABELLE_TOOL" logo HOL
    12.6  
    12.7 -cp "$ISABELLE_HOME/src/Doc/proof.sty" .
    12.8  cp "$ISABELLE_HOME/src/Doc/ttbox.sty" .
    12.9  cp "$ISABELLE_HOME/src/Doc/manual.bib" .
   12.10  

    13.1 --- a/src/Doc/ZF/document/build	Fri Dec 07 17:00:40 2012 +0100
    13.2 +++ b/src/Doc/ZF/document/build	Fri Dec 07 18:05:24 2012 +0100
    13.3 @@ -9,7 +9,6 @@
    13.4  
    13.5  cp "$ISABELLE_HOME/src/Doc/isar.sty" .
    13.6  cp "$ISABELLE_HOME/src/Doc/ttbox.sty" .
    13.7 -cp "$ISABELLE_HOME/src/Doc/proof.sty" .
    13.8  cp "$ISABELLE_HOME/src/Doc/manual.bib" .
    13.9  cp "$ISABELLE_HOME/src/Doc/Logics/document/syntax.tex" .
   13.10  

    14.1 --- a/src/Doc/proof.sty	Fri Dec 07 17:00:40 2012 +0100
    14.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    14.3 @@ -1,272 +0,0 @@
    14.4 -\ProvidesPackage{proof}[1995/05/22]
    14.5 -%       proof.sty       (Proof Figure Macros)
    14.6 -%
    14.7 -%       version 2.0
    14.8 -%       June 24, 1991
    14.9 -%       Copyright (C) 1990,1991 Makoto Tatsuta (tatsuta@riec.tohoku.ac.jp)
   14.10 -%
   14.11 -%Modified for LaTeX-2e by L. C. Paulson
   14.12 -% 
   14.13 -% This program is free software; you can redistribute it or modify
   14.14 -% it under the terms of the GNU General Public License as published by
   14.15 -% the Free Software Foundation; either versions 1, or (at your option)
   14.16 -% any later version.
   14.17 -% 
   14.18 -% This program is distributed in the hope that it will be useful
   14.19 -% but WITHOUT ANY WARRANTY; without even the implied warranty of
   14.20 -% MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
   14.21 -% GNU General Public License for more details.
   14.22 -%
   14.23 -%       Usage:
   14.24 -%               In \documentstyle, specify an optional style `proof', say,
   14.25 -%                       \documentstyle[proof]{article}.
   14.26 -%
   14.27 -%       The following macros are available:
   14.28 -%
   14.29 -%       In all the following macros, all the arguments such as
   14.30 -%       <Lowers> and <Uppers> are processed in math mode.
   14.31 -%
   14.32 -%       \infer<Lower><Uppers>
   14.33 -%               draws an inference.
   14.34 -%
   14.35 -%               Use & in <Uppers> to delimit upper formulae.
   14.36 -%               <Uppers> consists more than 0 formulae.
   14.37 -%
   14.38 -%               \infer returns \hbox{ ... } or \vbox{ ... } and
   14.39 -%               sets \@LeftOffset and \@RightOffset globally.
   14.40 -%
   14.41 -%       \infer[<Label>]<Lower><Uppers>
   14.42 -%               draws an inference labeled with <Label>.
   14.43 -%
   14.44 -%       \infer*<Lower><Uppers>
   14.45 -%               draws a many step deduction.
   14.46 -%
   14.47 -%       \infer*[<Label>]<Lower><Uppers>
   14.48 -%               draws a many step deduction labeled with <Label>.
   14.49 -%
   14.50 -%       \infer=<Lower><Uppers>
   14.51 -%               draws a double-ruled deduction.
   14.52 -%
   14.53 -%       \infer=[<Label>]<Lower><Uppers>
   14.54 -%               draws a double-ruled deduction labeled with <Label>.
   14.55 -%
   14.56 -%       \deduce<Lower><Uppers>
   14.57 -%               draws an inference without a rule.
   14.58 -%
   14.59 -%       \deduce[<Proof>]<Lower><Uppers>
   14.60 -%               draws a many step deduction with a proof name.
   14.61 -%
   14.62 -%       Example:
   14.63 -%               If you want to write
   14.64 -%                           B C
   14.65 -%                          -----
   14.66 -%                      A     D
   14.67 -%                     ----------
   14.68 -%                         E
   14.69 -%       use
   14.70 -%               \infer{E}{
   14.71 -%                       A
   14.72 -%                       &
   14.73 -%                       \infer{D}{B & C}
   14.74 -%               }
   14.75 -%
   14.76 -
   14.77 -%       Style Parameters
   14.78 -
   14.79 -\newdimen\inferLineSkip         \inferLineSkip=2pt
   14.80 -\newdimen\inferLabelSkip        \inferLabelSkip=5pt
   14.81 -\def\inferTabSkip{\quad}
   14.82 -
   14.83 -%       Variables
   14.84 -
   14.85 -\newdimen\@LeftOffset   % global
   14.86 -\newdimen\@RightOffset  % global
   14.87 -\newdimen\@SavedLeftOffset      % safe from users
   14.88 -
   14.89 -\newdimen\UpperWidth
   14.90 -\newdimen\LowerWidth
   14.91 -\newdimen\LowerHeight
   14.92 -\newdimen\UpperLeftOffset
   14.93 -\newdimen\UpperRightOffset
   14.94 -\newdimen\UpperCenter
   14.95 -\newdimen\LowerCenter
   14.96 -\newdimen\UpperAdjust
   14.97 -\newdimen\RuleAdjust
   14.98 -\newdimen\LowerAdjust
   14.99 -\newdimen\RuleWidth
  14.100 -\newdimen\HLabelAdjust
  14.101 -\newdimen\VLabelAdjust
  14.102 -\newdimen\WidthAdjust
  14.103 -
  14.104 -\newbox\@UpperPart
  14.105 -\newbox\@LowerPart
  14.106 -\newbox\@LabelPart
  14.107 -\newbox\ResultBox
  14.108 -
  14.109 -%       Flags
  14.110 -
  14.111 -\newif\if@inferRule     % whether \@infer draws a rule.
  14.112 -\newif\if@DoubleRule    % whether \@infer draws doulbe rules.
  14.113 -\newif\if@ReturnLeftOffset      % whether \@infer returns \@LeftOffset.
  14.114 -\newif\if@MathSaved     % whether inner math mode where \infer or
  14.115 -                        % \deduce appears.
  14.116 -
  14.117 -%       Special Fonts
  14.118 -
  14.119 -\def\DeduceSym{\vtop{\baselineskip4\p@ \lineskiplimit\z@
  14.120 -    \vbox{\hbox{.}\hbox{.}\hbox{.}}\hbox{.}}}
  14.121 -
  14.122 -%       Math Save Macros
  14.123 -%
  14.124 -%       \@SaveMath is called in the very begining of toplevel macros
  14.125 -%       which are \infer and \deduce.
  14.126 -%       \@RestoreMath is called in the very last before toplevel macros end.
  14.127 -%       Remark \infer and \deduce ends calling \@infer.
  14.128 -%TEMPORARILY DELETED BY LCP DUE TO CONFLICT WITH CLASS "amsmath.sty"
  14.129 -
  14.130 -\def\@SaveMath{}
  14.131 -
  14.132 -\def\@RestoreMath{}
  14.133 -
  14.134 -%       Macros
  14.135 -
  14.136 -\def\@ifEmpty#1#2#3{\def\@tempa{\@empty}\def\@tempb{#1}\relax
  14.137 -        \ifx \@tempa \@tempb #2\else #3\fi }
  14.138 -
  14.139 -\def\infer{\@SaveMath \@ifnextchar *{\@inferSteps}{\relax
  14.140 -        \@ifnextchar ={\@inferDoubleRule}{\@inferOneStep}}}
  14.141 -
  14.142 -\def\@inferOneStep{\@inferRuletrue \@DoubleRulefalse
  14.143 -        \@ifnextchar [{\@infer}{\@infer[\@empty]}}
  14.144 -
  14.145 -\def\@inferDoubleRule={\@inferRuletrue \@DoubleRuletrue
  14.146 -        \@ifnextchar [{\@infer}{\@infer[\@empty]}}
  14.147 -
  14.148 -\def\@inferSteps*{\@ifnextchar [{\@@inferSteps}{\@@inferSteps[\@empty]}}
  14.149 -
  14.150 -\def\@@inferSteps[#1]{\@deduce{#1}[\DeduceSym]}
  14.151 -
  14.152 -\def\deduce{\@SaveMath \@ifnextchar [{\@deduce{\@empty}}
  14.153 -        {\@inferRulefalse \@infer[\@empty]}}
  14.154 -
  14.155 -%       \@deduce<Proof Label>[<Proof>]<Lower><Uppers>
  14.156 -
  14.157 -\def\@deduce#1[#2]#3#4{\@inferRulefalse
  14.158 -        \@infer[\@empty]{#3}{\@SaveMath \@infer[{#1}]{#2}{#4}}}
  14.159 -
  14.160 -%       \@infer[<Label>]<Lower><Uppers>
  14.161 -%               If \@inferRuletrue, it draws a rule and <Label> is right to
  14.162 -%               a rule. In this case, if \@DoubleRuletrue, it draws
  14.163 -%               double rules.
  14.164 -%
  14.165 -%               Otherwise, draws no rule and <Label> is right to <Lower>.
  14.166 -
  14.167 -\def\@infer[#1]#2#3{\relax
  14.168 -% Get parameters
  14.169 -        \if@ReturnLeftOffset \else \@SavedLeftOffset=\@LeftOffset \fi
  14.170 -        \setbox\@LabelPart=\hbox{$#1$}\relax
  14.171 -        \setbox\@LowerPart=\hbox{$#2$}\relax
  14.172 -%
  14.173 -        \global\@LeftOffset=0pt
  14.174 -        \setbox\@UpperPart=\vbox{\tabskip=0pt \halign{\relax
  14.175 -                \global\@RightOffset=0pt \@ReturnLeftOffsettrue $##$&&
  14.176 -                \inferTabSkip
  14.177 -                \global\@RightOffset=0pt \@ReturnLeftOffsetfalse $##$\cr
  14.178 -                #3\cr}}\relax
  14.179 -%                       Here is a little trick.
  14.180 -%                       \@ReturnLeftOffsettrue(false) influences on \infer or
  14.181 -%                       \deduce placed in ## locally
  14.182 -%                       because of \@SaveMath and \@RestoreMath.
  14.183 -        \UpperLeftOffset=\@LeftOffset
  14.184 -        \UpperRightOffset=\@RightOffset
  14.185 -% Calculate Adjustments
  14.186 -        \LowerWidth=\wd\@LowerPart
  14.187 -        \LowerHeight=\ht\@LowerPart
  14.188 -        \LowerCenter=0.5\LowerWidth
  14.189 -%
  14.190 -        \UpperWidth=\wd\@UpperPart \advance\UpperWidth by -\UpperLeftOffset
  14.191 -        \advance\UpperWidth by -\UpperRightOffset
  14.192 -        \UpperCenter=\UpperLeftOffset
  14.193 -        \advance\UpperCenter by 0.5\UpperWidth
  14.194 -%
  14.195 -        \ifdim \UpperWidth > \LowerWidth
  14.196 -                % \UpperCenter > \LowerCenter
  14.197 -        \UpperAdjust=0pt
  14.198 -        \RuleAdjust=\UpperLeftOffset
  14.199 -        \LowerAdjust=\UpperCenter \advance\LowerAdjust by -\LowerCenter
  14.200 -        \RuleWidth=\UpperWidth
  14.201 -        \global\@LeftOffset=\LowerAdjust
  14.202 -%
  14.203 -        \else   % \UpperWidth <= \LowerWidth
  14.204 -        \ifdim \UpperCenter > \LowerCenter
  14.205 -%
  14.206 -        \UpperAdjust=0pt
  14.207 -        \RuleAdjust=\UpperCenter \advance\RuleAdjust by -\LowerCenter
  14.208 -        \LowerAdjust=\RuleAdjust
  14.209 -        \RuleWidth=\LowerWidth
  14.210 -        \global\@LeftOffset=\LowerAdjust
  14.211 -%
  14.212 -        \else   % \UpperWidth <= \LowerWidth
  14.213 -                % \UpperCenter <= \LowerCenter
  14.214 -%
  14.215 -        \UpperAdjust=\LowerCenter \advance\UpperAdjust by -\UpperCenter
  14.216 -        \RuleAdjust=0pt
  14.217 -        \LowerAdjust=0pt
  14.218 -        \RuleWidth=\LowerWidth
  14.219 -        \global\@LeftOffset=0pt
  14.220 -%
  14.221 -        \fi\fi
  14.222 -% Make a box
  14.223 -        \if@inferRule
  14.224 -%
  14.225 -        \setbox\ResultBox=\vbox{
  14.226 -                \moveright \UpperAdjust \box\@UpperPart
  14.227 -                \nointerlineskip \kern\inferLineSkip
  14.228 -                \if@DoubleRule
  14.229 -                \moveright \RuleAdjust \vbox{\hrule width\RuleWidth
  14.230 -                        \kern 1pt\hrule width\RuleWidth}\relax
  14.231 -                \else
  14.232 -                \moveright \RuleAdjust \vbox{\hrule width\RuleWidth}\relax
  14.233 -                \fi
  14.234 -                \nointerlineskip \kern\inferLineSkip
  14.235 -                \moveright \LowerAdjust \box\@LowerPart }\relax
  14.236 -%
  14.237 -        \@ifEmpty{#1}{}{\relax
  14.238 -%
  14.239 -        \HLabelAdjust=\wd\ResultBox     \advance\HLabelAdjust by -\RuleAdjust
  14.240 -        \advance\HLabelAdjust by -\RuleWidth
  14.241 -        \WidthAdjust=\HLabelAdjust
  14.242 -        \advance\WidthAdjust by -\inferLabelSkip
  14.243 -        \advance\WidthAdjust by -\wd\@LabelPart
  14.244 -        \ifdim \WidthAdjust < 0pt \WidthAdjust=0pt \fi
  14.245 -%
  14.246 -        \VLabelAdjust=\dp\@LabelPart
  14.247 -        \advance\VLabelAdjust by -\ht\@LabelPart
  14.248 -        \VLabelAdjust=0.5\VLabelAdjust  \advance\VLabelAdjust by \LowerHeight
  14.249 -        \advance\VLabelAdjust by \inferLineSkip
  14.250 -%
  14.251 -        \setbox\ResultBox=\hbox{\box\ResultBox
  14.252 -                \kern -\HLabelAdjust \kern\inferLabelSkip
  14.253 -                \raise\VLabelAdjust \box\@LabelPart \kern\WidthAdjust}\relax
  14.254 -%
  14.255 -        }\relax % end @ifEmpty
  14.256 -%
  14.257 -        \else % \@inferRulefalse
  14.258 -%
  14.259 -        \setbox\ResultBox=\vbox{
  14.260 -                \moveright \UpperAdjust \box\@UpperPart
  14.261 -                \nointerlineskip \kern\inferLineSkip
  14.262 -                \moveright \LowerAdjust \hbox{\unhbox\@LowerPart
  14.263 -                        \@ifEmpty{#1}{}{\relax
  14.264 -                        \kern\inferLabelSkip \unhbox\@LabelPart}}}\relax
  14.265 -        \fi
  14.266 -%
  14.267 -        \global\@RightOffset=\wd\ResultBox
  14.268 -        \global\advance\@RightOffset by -\@LeftOffset
  14.269 -        \global\advance\@RightOffset by -\LowerWidth
  14.270 -        \if@ReturnLeftOffset \else \global\@LeftOffset=\@SavedLeftOffset \fi
  14.271 -%
  14.272 -        \box\ResultBox
  14.273 -        \@RestoreMath
  14.274 -}
  14.275 -\endinput