Initial commit

6 files changed, 1179 insertions, 0 deletions

diff --git a/macros/latex/contrib/bussproofs-extra/LICENSE.txt b/macros/latex/contrib/bussproofs-extra/LICENSE.txt
new file mode 100644
index 0000000000..2244313901
--- /dev/null
+++ b/macros/latex/contrib/bussproofs-extra/LICENSE.txt
@@ -0,0 +1,416 @@
+The LaTeX Project Public License
+=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-
+
+LPPL Version 1.3c  2008-05-04
+
+Copyright 1999 2002-2008 LaTeX3 Project
+    Everyone is allowed to distribute verbatim copies of this
+    license document, but modification of it is not allowed.
+
+
+PREAMBLE
+========
+
+The LaTeX Project Public License (LPPL) is the primary license under
+which the LaTeX kernel and the base LaTeX packages are distributed.
+
+You may use this license for any work of which you hold the copyright
+and which you wish to distribute.  This license may be particularly
+suitable if your work is TeX-related (such as a LaTeX package), but 
+it is written in such a way that you can use it even if your work is 
+unrelated to TeX.
+
+The section `WHETHER AND HOW TO DISTRIBUTE WORKS UNDER THIS LICENSE',
+below, gives instructions, examples, and recommendations for authors
+who are considering distributing their works under this license.
+
+This license gives conditions under which a work may be distributed
+and modified, as well as conditions under which modified versions of
+that work may be distributed.
+
+We, the LaTeX3 Project, believe that the conditions below give you
+the freedom to make and distribute modified versions of your work
+that conform with whatever technical specifications you wish while
+maintaining the availability, integrity, and reliability of
+that work.  If you do not see how to achieve your goal while
+meeting these conditions, then read the document `cfgguide.tex'
+and `modguide.tex' in the base LaTeX distribution for suggestions.
+
+
+DEFINITIONS
+===========
+
+In this license document the following terms are used:
+
+   `Work'
+    Any work being distributed under this License.
+    
+   `Derived Work'
+    Any work that under any applicable law is derived from the Work.
+
+   `Modification' 
+    Any procedure that produces a Derived Work under any applicable
+    law -- for example, the production of a file containing an
+    original file associated with the Work or a significant portion of
+    such a file, either verbatim or with modifications and/or
+    translated into another language.
+
+   `Modify'
+    To apply any procedure that produces a Derived Work under any
+    applicable law.
+    
+   `Distribution'
+    Making copies of the Work available from one person to another, in
+    whole or in part.  Distribution includes (but is not limited to)
+    making any electronic components of the Work accessible by
+    file transfer protocols such as FTP or HTTP or by shared file
+    systems such as Sun's Network File System (NFS).
+
+   `Compiled Work'
+    A version of the Work that has been processed into a form where it
+    is directly usable on a computer system.  This processing may
+    include using installation facilities provided by the Work,
+    transformations of the Work, copying of components of the Work, or
+    other activities.  Note that modification of any installation
+    facilities provided by the Work constitutes modification of the Work.
+
+   `Current Maintainer'
+    A person or persons nominated as such within the Work.  If there is
+    no such explicit nomination then it is the `Copyright Holder' under
+    any applicable law.
+
+   `Base Interpreter' 
+    A program or process that is normally needed for running or
+    interpreting a part or the whole of the Work.    
+
+    A Base Interpreter may depend on external components but these
+    are not considered part of the Base Interpreter provided that each
+    external component clearly identifies itself whenever it is used
+    interactively.  Unless explicitly specified when applying the
+    license to the Work, the only applicable Base Interpreter is a
+    `LaTeX-Format' or in the case of files belonging to the 
+    `LaTeX-format' a program implementing the `TeX language'.
+
+
+
+CONDITIONS ON DISTRIBUTION AND MODIFICATION
+===========================================
+
+1.  Activities other than distribution and/or modification of the Work
+are not covered by this license; they are outside its scope.  In
+particular, the act of running the Work is not restricted and no
+requirements are made concerning any offers of support for the Work.
+
+2.  You may distribute a complete, unmodified copy of the Work as you
+received it.  Distribution of only part of the Work is considered
+modification of the Work, and no right to distribute such a Derived
+Work may be assumed under the terms of this clause.
+
+3.  You may distribute a Compiled Work that has been generated from a
+complete, unmodified copy of the Work as distributed under Clause 2
+above, as long as that Compiled Work is distributed in such a way that
+the recipients may install the Compiled Work on their system exactly
+as it would have been installed if they generated a Compiled Work
+directly from the Work.
+
+4.  If you are the Current Maintainer of the Work, you may, without
+restriction, modify the Work, thus creating a Derived Work.  You may
+also distribute the Derived Work without restriction, including
+Compiled Works generated from the Derived Work.  Derived Works
+distributed in this manner by the Current Maintainer are considered to
+be updated versions of the Work.
+
+5.  If you are not the Current Maintainer of the Work, you may modify
+your copy of the Work, thus creating a Derived Work based on the Work,
+and compile this Derived Work, thus creating a Compiled Work based on
+the Derived Work.
+
+6.  If you are not the Current Maintainer of the Work, you may
+distribute a Derived Work provided the following conditions are met
+for every component of the Work unless that component clearly states
+in the copyright notice that it is exempt from that condition.  Only
+the Current Maintainer is allowed to add such statements of exemption 
+to a component of the Work. 
+
+  a. If a component of this Derived Work can be a direct replacement
+     for a component of the Work when that component is used with the
+     Base Interpreter, then, wherever this component of the Work
+     identifies itself to the user when used interactively with that
+     Base Interpreter, the replacement component of this Derived Work
+     clearly and unambiguously identifies itself as a modified version
+     of this component to the user when used interactively with that
+     Base Interpreter.
+     
+  b. Every component of the Derived Work contains prominent notices
+     detailing the nature of the changes to that component, or a
+     prominent reference to another file that is distributed as part
+     of the Derived Work and that contains a complete and accurate log
+     of the changes.
+  
+  c. No information in the Derived Work implies that any persons,
+     including (but not limited to) the authors of the original version
+     of the Work, provide any support, including (but not limited to)
+     the reporting and handling of errors, to recipients of the
+     Derived Work unless those persons have stated explicitly that
+     they do provide such support for the Derived Work.
+
+  d. You distribute at least one of the following with the Derived Work:
+
+       1. A complete, unmodified copy of the Work; 
+          if your distribution of a modified component is made by
+          offering access to copy the modified component from a
+          designated place, then offering equivalent access to copy
+          the Work from the same or some similar place meets this
+          condition, even though third parties are not compelled to
+          copy the Work along with the modified component;
+
+       2. Information that is sufficient to obtain a complete,
+          unmodified copy of the Work.
+
+7.  If you are not the Current Maintainer of the Work, you may
+distribute a Compiled Work generated from a Derived Work, as long as
+the Derived Work is distributed to all recipients of the Compiled
+Work, and as long as the conditions of Clause 6, above, are met with
+regard to the Derived Work.
+
+8.  The conditions above are not intended to prohibit, and hence do not
+apply to, the modification, by any method, of any component so that it
+becomes identical to an updated version of that component of the Work as
+it is distributed by the Current Maintainer under Clause 4, above.
+
+9.  Distribution of the Work or any Derived Work in an alternative
+format, where the Work or that Derived Work (in whole or in part) is
+then produced by applying some process to that format, does not relax or
+nullify any sections of this license as they pertain to the results of
+applying that process.
+     
+10. a. A Derived Work may be distributed under a different license
+       provided that license itself honors the conditions listed in
+       Clause 6 above, in regard to the Work, though it does not have
+       to honor the rest of the conditions in this license.
+      
+    b. If a Derived Work is distributed under a different license, that
+       Derived Work must provide sufficient documentation as part of
+       itself to allow each recipient of that Derived Work to honor the 
+       restrictions in Clause 6 above, concerning changes from the Work.
+
+11. This license places no restrictions on works that are unrelated to
+the Work, nor does this license place any restrictions on aggregating
+such works with the Work by any means.
+
+12.  Nothing in this license is intended to, or may be used to, prevent
+complete compliance by all parties with all applicable laws.
+
+
+NO WARRANTY
+===========
+
+There is no warranty for the Work.  Except when otherwise stated in
+writing, the Copyright Holder provides the Work `as is', without
+warranty of any kind, either expressed or implied, including, but not
+limited to, the implied warranties of merchantability and fitness for a
+particular purpose.  The entire risk as to the quality and performance
+of the Work is with you.  Should the Work prove defective, you assume
+the cost of all necessary servicing, repair, or correction.
+
+In no event unless required by applicable law or agreed to in writing
+will The Copyright Holder, or any author named in the components of the
+Work, or any other party who may distribute and/or modify the Work as
+permitted above, be liable to you for damages, including any general,
+special, incidental or consequential damages arising out of any use of
+the Work or out of inability to use the Work (including, but not limited
+to, loss of data, data being rendered inaccurate, or losses sustained by
+anyone as a result of any failure of the Work to operate with any other
+programs), even if the Copyright Holder or said author or said other
+party has been advised of the possibility of such damages.
+
+
+MAINTENANCE OF THE WORK
+=======================
+
+The Work has the status `author-maintained' if the Copyright Holder
+explicitly and prominently states near the primary copyright notice in
+the Work that the Work can only be maintained by the Copyright Holder
+or simply that it is `author-maintained'.
+
+The Work has the status `maintained' if there is a Current Maintainer
+who has indicated in the Work that they are willing to receive error
+reports for the Work (for example, by supplying a valid e-mail
+address). It is not required for the Current Maintainer to acknowledge
+or act upon these error reports.
+
+The Work changes from status `maintained' to `unmaintained' if there
+is no Current Maintainer, or the person stated to be Current
+Maintainer of the work cannot be reached through the indicated means
+of communication for a period of six months, and there are no other
+significant signs of active maintenance.
+
+You can become the Current Maintainer of the Work by agreement with
+any existing Current Maintainer to take over this role.
+
+If the Work is unmaintained, you can become the Current Maintainer of
+the Work through the following steps:
+
+ 1.  Make a reasonable attempt to trace the Current Maintainer (and
+     the Copyright Holder, if the two differ) through the means of
+     an Internet or similar search.
+
+ 2.  If this search is successful, then enquire whether the Work
+     is still maintained.
+
+  a. If it is being maintained, then ask the Current Maintainer
+     to update their communication data within one month.
+     
+  b. If the search is unsuccessful or no action to resume active
+     maintenance is taken by the Current Maintainer, then announce
+     within the pertinent community your intention to take over
+     maintenance.  (If the Work is a LaTeX work, this could be
+     done, for example, by posting to comp.text.tex.)
+
+ 3a. If the Current Maintainer is reachable and agrees to pass
+     maintenance of the Work to you, then this takes effect
+     immediately upon announcement.
+     
+  b. If the Current Maintainer is not reachable and the Copyright
+     Holder agrees that maintenance of the Work be passed to you,
+     then this takes effect immediately upon announcement.  
+    
+ 4.  If you make an `intention announcement' as described in 2b. above
+     and after three months your intention is challenged neither by
+     the Current Maintainer nor by the Copyright Holder nor by other
+     people, then you may arrange for the Work to be changed so as
+     to name you as the (new) Current Maintainer.
+     
+ 5.  If the previously unreachable Current Maintainer becomes
+     reachable once more within three months of a change completed
+     under the terms of 3b) or 4), then that Current Maintainer must
+     become or remain the Current Maintainer upon request provided
+     they then update their communication data within one month.
+
+A change in the Current Maintainer does not, of itself, alter the fact
+that the Work is distributed under the LPPL license.
+
+If you become the Current Maintainer of the Work, you should
+immediately provide, within the Work, a prominent and unambiguous
+statement of your status as Current Maintainer.  You should also
+announce your new status to the same pertinent community as
+in 2b) above.
+
+
+WHETHER AND HOW TO DISTRIBUTE WORKS UNDER THIS LICENSE
+======================================================
+
+This section contains important instructions, examples, and
+recommendations for authors who are considering distributing their
+works under this license.  These authors are addressed as `you' in
+this section.
+
+Choosing This License or Another License
+----------------------------------------
+
+If for any part of your work you want or need to use *distribution*
+conditions that differ significantly from those in this license, then
+do not refer to this license anywhere in your work but, instead,
+distribute your work under a different license.  You may use the text
+of this license as a model for your own license, but your license
+should not refer to the LPPL or otherwise give the impression that
+your work is distributed under the LPPL.
+
+The document `modguide.tex' in the base LaTeX distribution explains
+the motivation behind the conditions of this license.  It explains,
+for example, why distributing LaTeX under the GNU General Public
+License (GPL) was considered inappropriate.  Even if your work is
+unrelated to LaTeX, the discussion in `modguide.tex' may still be
+relevant, and authors intending to distribute their works under any
+license are encouraged to read it.
+
+A Recommendation on Modification Without Distribution
+-----------------------------------------------------
+
+It is wise never to modify a component of the Work, even for your own
+personal use, without also meeting the above conditions for
+distributing the modified component.  While you might intend that such
+modifications will never be distributed, often this will happen by
+accident -- you may forget that you have modified that component; or
+it may not occur to you when allowing others to access the modified
+version that you are thus distributing it and violating the conditions
+of this license in ways that could have legal implications and, worse,
+cause problems for the community.  It is therefore usually in your
+best interest to keep your copy of the Work identical with the public
+one.  Many works provide ways to control the behavior of that work
+without altering any of its licensed components.
+
+How to Use This License
+-----------------------
+
+To use this license, place in each of the components of your work both
+an explicit copyright notice including your name and the year the work
+was authored and/or last substantially modified.  Include also a
+statement that the distribution and/or modification of that
+component is constrained by the conditions in this license.
+
+Here is an example of such a notice and statement:
+
+  %% pig.dtx
+  %% Copyright 2005 M. Y. Name
+  %
+  % This work may be distributed and/or modified under the
+  % conditions of the LaTeX Project Public License, either version 1.3
+  % of this license or (at your option) any later version.
+  % The latest version of this license is in
+  %   http://www.latex-project.org/lppl.txt
+  % and version 1.3 or later is part of all distributions of LaTeX
+  % version 2005/12/01 or later.
+  %
+  % This work has the LPPL maintenance status `maintained'.
+  % 
+  % The Current Maintainer of this work is M. Y. Name.
+  %
+  % This work consists of the files pig.dtx and pig.ins
+  % and the derived file pig.sty.
+
+Given such a notice and statement in a file, the conditions
+given in this license document would apply, with the `Work' referring
+to the three files `pig.dtx', `pig.ins', and `pig.sty' (the last being
+generated from `pig.dtx' using `pig.ins'), the `Base Interpreter'
+referring to any `LaTeX-Format', and both `Copyright Holder' and
+`Current Maintainer' referring to the person `M. Y. Name'.
+
+If you do not want the Maintenance section of LPPL to apply to your
+Work, change `maintained' above into `author-maintained'.  
+However, we recommend that you use `maintained', as the Maintenance
+section was added in order to ensure that your Work remains useful to
+the community even when you can no longer maintain and support it
+yourself.
+
+Derived Works That Are Not Replacements
+---------------------------------------
+
+Several clauses of the LPPL specify means to provide reliability and
+stability for the user community. They therefore concern themselves
+with the case that a Derived Work is intended to be used as a
+(compatible or incompatible) replacement of the original Work. If
+this is not the case (e.g., if a few lines of code are reused for a
+completely different task), then clauses 6b and 6d shall not apply.
+
+
+Important Recommendations
+-------------------------
+
+ Defining What Constitutes the Work
+
+   The LPPL requires that distributions of the Work contain all the
+   files of the Work.  It is therefore important that you provide a
+   way for the licensee to determine which files constitute the Work.
+   This could, for example, be achieved by explicitly listing all the
+   files of the Work near the copyright notice of each file or by
+   using a line such as:
+
+    % This work consists of all files listed in manifest.txt.
+   
+   in that place.  In the absence of an unequivocal list it might be
+   impossible for the licensee to determine what is considered by you
+   to comprise the Work and, in such a case, the licensee would be
+   entitled to make reasonable conjectures as to which files comprise
+   the Work.
+
diff --git a/macros/latex/contrib/bussproofs-extra/README.md b/macros/latex/contrib/bussproofs-extra/README.md
new file mode 100644
index 0000000000..a9a6d58b2f
--- /dev/null
+++ b/macros/latex/contrib/bussproofs-extra/README.md
@@ -0,0 +1,16 @@
+bussproofs-extra
+================
+
+Additional functionality for bussproofs.sty. Specifically, it allows
+for typesetting of entire (sub)deductions.
+
+To install, download the files, and run 
+```
+latex bussproofs-extra.ins
+```
+To generate the documentation, run
+```
+pdflatex bussproofs-extra.dtx
+```
+
+This package is distributed under the terms of the LPPL 1.3c
diff --git a/macros/latex/contrib/bussproofs-extra/bpextra.sty b/macros/latex/contrib/bussproofs-extra/bpextra.sty
new file mode 100644
index 0000000000..e83935d50d
--- /dev/null
+++ b/macros/latex/contrib/bussproofs-extra/bpextra.sty
@@ -0,0 +1,5 @@
+% Wrapper for backwards compatibility
+
+\RequirePackage{bussproofs-extra}
+\PackageWarning{bussproofs-extra}{You've loaded bussproofs with
+  bpextra, but you should use bussproofs-extra instead}
diff --git a/macros/latex/contrib/bussproofs-extra/bussproofs-extra.dtx b/macros/latex/contrib/bussproofs-extra/bussproofs-extra.dtx
new file mode 100644
index 0000000000..a371cff408
--- /dev/null
+++ b/macros/latex/contrib/bussproofs-extra/bussproofs-extra.dtx
@@ -0,0 +1,685 @@
+% \iffalse meta-comment
+%
+%
+% Copyright (C) 2019 by Richard Zach <rzach@ucalgary.ca>
+% ------------------------------------------------------
+%
+% This work may be distributed and/or modified under the
+% conditions of the LaTeX Project Public License, either version 1.3
+% of this license or (at your option) any later version.
+% The latest version of this license is in
+%   http://www.latex-project.org/lppl.txt
+% and version 1.3 or later is part of all distributions of LaTeX
+% version 2005/12/01 or later.
+%
+% This work has the LPPL maintenance status `maintained'.
+% 
+% The Current Maintainer of this work is Richard Zach.
+%
+% This work consists of the files bussproofs-pextra.dtx,
+% bussproofs-extra.ins, bussproofs-extra.sty
+%
+% \fi
+%
+% \iffalse
+%<*driver>
+\ProvidesFile{bussproofs-extra.dtx}
+%</driver>
+%<package>\NeedsTeXFormat{LaTeX2e}
+%<package>\ProvidesPackage{bussproofs-extra}
+%<package>   [2019/05/31 0.4 Extra commands for bussproofs.sty]
+%<*driver>
+\documentclass{ltxdoc}
+
+\usepackage{bussproofs-extra}
+\usepackage[colorlinks,allcolors=blue]{hyperref}
+\usepackage{calc}
+
+\renewcommand{\fCenter}{\ensuremath{\,{\to}\,}}
+
+\EnableCrossrefs         
+\RecordChanges
+\begin{document}
+  \DocInput{bussproofs-extra.dtx}
+  \PrintChanges
+\end{document}
+%</driver>
+% \fi
+%
+% \CheckSum{0}
+%
+% \CharacterTable
+%  {Upper-case    \A\B\C\D\E\F\G\H\I\J\K\L\M\N\O\P\Q\R\S\T\U\V\W\X\Y\Z
+%   Lower-case    \a\b\c\d\e\f\g\h\i\j\k\l\m\n\o\p\q\r\s\t\u\v\w\x\y\z
+%   Digits        \0\1\2\3\4\5\6\7\8\9
+%   Exclamation   \!     Double quote  \"     Hash (number) \#
+%   Dollar        \$     Percent       \%     Ampersand     \&
+%   Acute accent  \'     Left paren    \(     Right paren   \)
+%   Asterisk      \*     Plus          \+     Comma         \,
+%   Minus         \-     Point         \.     Solidus       \/
+%   Colon         \:     Semicolon     \;     Less than     \<
+%   Equals        \=     Greater than  \>     Question mark \?
+%   Commercial at \@     Left bracket  \[     Backslash     \\
+%   Right bracket \]     Circumflex    \^     Underscore    \_
+%   Grave accent  \`     Left brace    \{     Vertical bar  \|
+%   Right brace   \}     Tilde         \~}
+%
+%
+% \changes{v0.4}{2019/05/31}{Better implementation of line labels; add
+% shortDeduce; style deduce lines} 
+% \changes{v0.3}{2019/04/04}{Rename to bussproofs-extra.sty} 
+% \changes{v0.2}{2014/10/16}{Fixed bug in dotsdDeduce, added examples}
+% \changes{v0.1}{2014/04/26}{Initial version with deduce, linelabel functionality}
+%
+% \GetFileInfo{bussproofs-extra.sty}
+%
+% \DoNotIndex{\newcommand,\newenvironment}
+%
+%
+% \title{The \textsf{bussproofs-extra} package\thanks{This document
+%   corresponds to \textsf{bussproofs-extra}~\fileversion, dated \filedate.}}
+% \author{\href{http://richardzach.org/}{Richard Zach}}
+% \date{}
+%
+% \maketitle
+%
+% \section{Introduction}
+%
+% The \textsf{bussproofs-extra} package provides additional functionality for
+% the proof tree typesetting package
+% \href{http://math.ucsd.edu/~sbuss/ResearchWeb/bussproofs/}{\textsf{bussproofs}}
+% by Sam Buss.  It is experimental and tested only with v.1.1, and
+% only in \LaTeX{} mode with upward-growing trees.
+% Functionality provided includes:
+%
+% \begin{enumerate}
+% \item |\Deduce$| and |\DeduceC| commands, which work much
+%  like |\Infer| commands but indicate missing parts of a proof.
+% \item Multiple styles for typesetting the result of |\Deduce|,
+% including 
+% \begin{enumerate}
+% \item |\straightDeduce|, which produces vertical dots
+% \item |\branchDeduce|, which produces diagonal plus vertical dots
+% \item |\ddotsDeduce|, which produces diagonal dots from top left
+%  to bottom right
+% \item |\dotsdDeduce|, which produces diagonal dots from top right
+%  to bottom left
+% \item |\shortDeduce|, which is like |\straightDeduce| but half the length
+% \end{enumerate}
+% |\straightDeduce| is the default.  It can be changed by redefining
+% |\alwaysDeduce|.
+% \item |\LeftLineLabel| and |\RightLineLabel| commands which
+%   work like |\LeftLabel| and |\RightLabel| but place a label
+%   next to the conclusion of an inference/deduction instead of the score
+%   line.
+% \item |\LeftSubproofLabel| and |\RightSubproofLabel| commands which
+%   work like |\LeftLabel| and |\RightLabel| but place a label
+%   next to the entire preceding subproof with a curly brace.
+% \end{enumerate}
+%
+% Here's what these deductions look like:
+%
+% \begin{center}
+% \begin{tabular}{@{}cccc@{}}
+% \fbox{\AxiomC{$A$}
+% \straightDeduce
+% \DeduceC{$B$}
+% \DisplayProof} &
+% \fbox{\AxiomC{$A$}
+% \branchDeduce
+% \DeduceC{$B$}
+% \DisplayProof} &
+% \fbox{\AxiomC{$A$}
+% \ddotsDeduce
+% \DeduceC{$B$}
+% \DisplayProof} &
+% \fbox{\AxiomC{$A$}
+% \dotsdDeduce
+% \DeduceC{$B$}
+% \DisplayProof} \\ \\
+% \fbox{\Axiom$A \fCenter B$
+% \straightDeduce
+% \Deduce$A \lor C \fCenter B$
+% \DisplayProof} &
+% \fbox{\Axiom$A \fCenter B$
+% \branchDeduce
+% \Deduce$A \lor C \fCenter B$
+% \DisplayProof} &
+% \fbox{\Axiom$A  \fCenter B$
+% \ddotsDeduce
+% \Deduce$A \lor C \fCenter B$
+% \DisplayProof} &
+% \fbox{\Axiom$A \fCenter B$
+% \dotsdDeduce
+% \Deduce$A \lor C \fCenter B$
+% \DisplayProof}
+% \\ \\
+% \texttt{straightDeduce} &
+% \texttt{branchDeduce} &
+% \texttt{ddotsDeduce} &
+% \texttt{dotsdDeduce} 
+% \end{tabular}
+% \end{center}
+%
+%
+% The most up-to-date version of this package is available at the
+% \href{https://github.com/OpenLogicProject/bussproofs-extra}{Open Logic
+% Project github site}, where you can file bug reports as well.
+%
+% \subsection{Example}
+%
+% \begin{verbatim}
+% \begin{prooftree}
+% \AxiomC{}
+% \RightLabel{$\pi_1(a)$}
+% \Deduce$\Gamma_1 \fCenter \Theta_1, F(a)$
+% \RightLabel{$\forall$R}
+% \UnaryInf$\Gamma_1 \fCenter \Theta_1, \forall x\,F(x)$
+% \ddotsDeduce
+% \RightLabel{$\pi_1'$}
+% \Deduce$\Gamma \fCenter \Theta, \forall x\,F(x)$
+% \AxiomC{}
+% \RightLabel{$\pi_2$}
+% \Deduce$F(n), \Delta_1 \fCenter \Lambda_1$
+% \RightLabel{$\forall$L}
+% \UnaryInf$\forall x\,F(x), \Delta_1 \fCenter \Lambda_1$
+% \dotsdDeduce
+% \RightLabel{$\pi_2'$}
+% \Deduce$\forall x\,F(x), \Delta \fCenter \Lambda$
+% \RightLabel{cut}
+% \BinaryInf$\Gamma, \Delta \fCenter \Theta, \Lambda$
+% \RightLabel{$\pi_4$}
+% \branchDeduce
+% \Deduce$\Pi \fCenter \Xi$
+% \end{prooftree}
+% \end{verbatim}
+% produces this:
+% \begin{prooftree}
+% \AxiomC{}
+% \RightLabel{$\pi_1(a)$}
+% \Deduce$\Gamma_1 \fCenter \Theta_1, F(a)$
+% \RightLabel{$\forall$R}
+% \UnaryInf$\Gamma_1 \fCenter \Theta_1, \forall x\,F(x)$
+% \ddotsDeduce
+% \RightLabel{$\pi_1'$}
+% \Deduce$\Gamma \fCenter \Theta, \forall x\,F(x)$
+% \AxiomC{}
+% \RightLabel{$\pi_2$}
+% \Deduce$F(n), \Delta_1 \fCenter \Lambda_1$
+% \RightLabel{$\forall$L}
+% \UnaryInf$\forall x\,F(x), \Delta_1 \fCenter \Lambda_1$
+% \dotsdDeduce
+% \RightLabel{$\pi_2'$}
+% \Deduce$\forall x\,F(x), \Delta \fCenter \Lambda$
+% \RightLabel{cut}
+% \BinaryInf$\Gamma, \Delta \fCenter \Theta, \Lambda$
+% \RightLabel{$\pi_4$}
+% \branchDeduce
+% \Deduce$\Pi \fCenter \Xi$
+% \end{prooftree}
+
+% It is also possible to label entire subproofs on the left and on the right.
+% \begin{verbatim}
+% \begin{prooftree}
+% \AxiomC{}
+% \Deduce$\Gamma \fCenter \Delta$
+% \LeftLineLabel{$S_1$}
+% \Deduce$\Gamma \fCenter \Delta, A$
+% \LeftSubproofLabel{$\pi$}
+% \AxiomC{}
+% \Deduce$\Gamma' \fCenter \Delta'$
+% \LeftLineLabel{$S_2$}
+% \Deduce$A, \Gamma' \fCenter \Delta'$
+% \RightSubproofLabel{$\pi'$}
+% \RightLabel{cut}
+% \LeftLineLabel{$S_3$}
+% \BinaryInf$\Gamma, \Gamma' \fCenter \Delta, \Delta'$
+% \Deduce$\Pi \fCenter \Lambda$
+% \end{prooftree}
+% \end{verbatim}
+% \begin{prooftree}
+% \AxiomC{}
+% \Deduce$\Gamma \fCenter \Delta$
+% \Deduce$\Gamma \fCenter \Delta, A$
+% \LeftSubproofLabel{$\pi$}
+% \AxiomC{}
+% \Deduce$\Gamma' \fCenter \Delta'$
+% \Deduce$A, \Gamma' \fCenter \Delta'$
+% \RightSubproofLabel{$\pi'$}
+% \RightLabel{cut}
+% \BinaryInf$\Gamma, \Gamma' \fCenter \Delta, \Delta'$
+% \Deduce$\Pi \fCenter \Lambda$
+% \end{prooftree}
+%
+% The |\LeftLineLabel| and |\RightLineLabel| commands add labels to
+% the sequent or formula produced by the following |\Axiom|, |\XxxxInf|,
+% and |\Deduce| command. 
+% \begin{prooftree}
+%    \LeftLineLabel{$S_1$}
+%    \RightLineLabel{$S_1$}
+%    \Axiom$\phantom{A, {}}\Gamma \fCenter \Delta$
+%    \LeftLineLabel{$S_2$}
+%    \RightLineLabel{$S_2$}
+%    \UnaryInf$A, \Gamma \fCenter \Delta, B$
+%    \LeftLineLabel{$S_3$}
+%    \Deduce$\Pi \fCenter \Lambda$
+%    \LeftLineLabel{$S_1'$}
+%    \AxiomC{\makebox[\widthof{$A \lor B$}][c]{$A$}}
+%    \LeftLineLabel{$S_2'$}
+%    \UnaryInfC{$A \lor B$}
+%    \LeftLineLabel{$S_3'$}
+%    \DeduceC{$C$}
+%    \LeftLineLabel{$S_4$}
+%    \BinaryInf$\Pi \fCenter \Lambda$
+%    \RightLineLabel{$S_5$}
+%    \UnaryInf$\Pi \fCenter \Lambda$
+% \end{prooftree}
+% If the sequent or formula is itself a premise of an |\XxxInf|
+% command and the conclusion is longer, this may produce a less 
+% than optimal result, as the label is produced before the score 
+% line below (compare the left and right labels of the top left
+% sequent above). In that case you may want to insert extra space 
+% using |\phantom|, or use |\makebox| and the |\widthof| command 
+% of the |calc| package for the |XxxC| variants of the commands 
+% (see the top right formula below) as in the |\Axiom| commands 
+% below.
+% \begin{verbatim}  
+% \begin{prooftree}
+%    \LeftLineLabel{$S_1$}
+%    \RightLineLabel{$S_1$}
+%    \Axiom$\phantom{A, {}}\Gamma \fCenter \Delta$
+%    \LeftLineLabel{$S_2$}
+%    \RightLineLabel{$S_2$}
+%    \UnaryInf$A, \Gamma \fCenter \Delta, B$
+%    \LeftLineLabel{$S_3$}
+%    \Deduce$\Pi \fCenter \Lambda$
+%    \LeftLineLabel{$S_1'$}
+%    \AxiomC{\makebox[\widthof{$A \lor B$}][c]{$A$}}
+%    \LeftLineLabel{$S_2'$}
+%    \UnaryInfC{$A \lor B$}
+%    \LeftLineLabel{$S_3'$}
+%    \DeduceC{$C$}
+%    \LeftLineLabel{$S_4$}
+%    \BinaryInf$\Pi \fCenter \Lambda$
+%    \RightLineLabel{$S_5$}
+%    \UnaryInf$\Pi \fCenter \Lambda$
+% \end{prooftree}    
+% \end{verbatim}    
+%
+% \StopEventually{}
+%
+% \section{Implementation}
+%
+% \subsection{Setup}
+% 
+% We require \textsf{bussproofs} (obviously) and and \textsf{tikz} for
+% drawing things.
+%
+%    \begin{macrocode}
+\RequirePackage{bussproofs}
+\RequirePackage{tikz}
+%    \end{macrocode}
+% \subsection{Dimensions and boxes}
+% 
+% \textsf{bussproofs} aligns sequents at the right end of the sequent
+% arrow, so we need to remember by how much to correct to get
+% deductions to the middle of sequents.  For |\ddotsDeduce| and
+% |\dotsdDeduce| (diagonal) styles, the upper and lower sequents will be
+% displaced.
+%    \begin{macrocode}
+\newdimen\CenterCorrection
+\newdimen\DiagCorrection
+%    \end{macrocode}
+% We need two boxes to hold the left and right line labels.
+%    \begin{macrocode}
+\newbox\myBoxLLL
+\newbox\myBoxRLL
+%    \end{macrocode} 
+% \subsection{Deduce Styles} 
+%
+% The following commands set the style for the next |\Deduce|
+% command. |\straightDeduce| produces a simple vertical line of dots,
+% and |\shortDeduce| a line of half that length.
+% |\branchDeduce| produces centered branching (Takeuti/Gentzen-style)
+% dots, |\ddotsDeduce| left-to-right diagonal dots, and |\dotsdDeduce|
+% right-to-left diagonal dots. They do this by redefining the
+% |\fDeduce| command which produces the dots and sets up the
+% dimensions. The TikZ style |deduceLine| is used as argument to the
+% |\draw| command and can be redefined for other line styles as well
+% (e.g., smaller dots or closer spacing).
+%    \begin{macrocode}
+\tikzset{
+    deduceLine/.style = {line width=1.1pt, loosely dotted}}
+
+\def\straightDeduce{%
+  \gdef\fDeduce{\tikz\draw[deduceLine] (0,0) -- (0,1);}
+  \global\DiagCorrection=0pt
+  \ignorespaces
+}
+
+\def\shortDeduce{%
+  \gdef\fDeduce{\tikz\draw[deduceLine] (0,0) -- (0,.5);}
+  \global\DiagCorrection=0pt
+  \ignorespaces
+}
+
+\def\branchDeduce{%
+  \gdef\fDeduce{\begin{tikzpicture}
+      \draw[deduceLine] (0,0) -- (0,1);
+      \draw[deduceLine] (-.5,.5) -- (0,0);
+      \draw[deduceLine] (.5,.5) -- (0,0);
+  \end{tikzpicture}}
+  \global\DiagCorrection=0pt
+  \ignorespaces
+}
+
+\def\ddotsDeduce{%
+  \gdef\fDeduce{\begin{tikzpicture}
+      \draw[deduceLine] (0,1) -- (1,0);
+  \end{tikzpicture}}
+  \setbox\myBoxA=\hbox{\fDeduce}
+  \global\DiagCorrection=-\wd\myBoxA
+  \ignorespaces
+}
+
+\def\dotsdDeduce{%
+  \gdef\fDeduce{\begin{tikzpicture}
+      \draw[deduceLine] (1,1) -- (0,0);
+  \end{tikzpicture}}
+  \setbox\myBoxA=\hbox{\fDeduce}
+  \global\DiagCorrection=\wd\myBoxA
+  \ignorespaces
+}
+%    \end{macrocode}
+% The |\alwaysDeduce| command is used to (re)set the
+% deduce style to a default and is executed every time a deduction is
+% typeset. It can be redefined to change the default deduce style.
+%    \begin{macrocode}
+\def\alwaysDeduce{\straightDeduce}
+\straightDeduce
+%    \end{macrocode}
+% \subsection{\texttt{\textbackslash Deduce\$} and
+% \texttt{\textbackslash DeduceC}}
+% 
+% |\Deduce$| and |\DeduceC| are the commands to actually produce the
+% deductions. They are used and work just like |\UnaryInf$| and
+% |\UnaryInfC|.
+%    \begin{macrocode}
+\def\Deduce$#1\fCenter#2${%
+    \prepUnary%
+    \buildConclusion{#1}{#2}%
+    \setbox\myBoxA=\hbox{\fCenter}%
+    \global\CenterCorrection=-.5\wd\myBoxA
+    \joinDeduce%
+    \resetInferenceDefaults%
+    \ignorespaces%
+}
+
+\def\DeduceC#1{
+    \prepUnary%
+    \buildConclusionC{#1}%
+    \global\CenterCorrection=0pt
+    \joinDeduce%
+    \resetInferenceDefaults%
+    \ignorespaces%
+}
+%    \end{macrocode}
+% \section{Typesetting the Deduction}
+% 
+% |\joinDeduce| aligns and joins |\curBox| and |\myBoxC| into a single
+% |vbox|.  |\curBox| holds the upper proof, |\curScoreStart| is
+% distance to where the line below the premise would start,
+% |\curScoreCenter| is distance from left edge of score to the 
+% alignment point, and |\curScoreEnd| is width of the score line.
+%    \begin{macrocode}
+
+\def\joinDeduce{%
+    \global\advance\curCenter by -\hypKernAmt%
+%    \end{macrocode}
+% If center of premise is left of center of conclusion move upper box
+% to right by difference, else move lower box right by difference
+%    \begin{macrocode}
+    \ifnum\curCenter<\newCenter%
+        \displace=\newCenter%
+        \advance \displace by -\curCenter%
+        \kernUpperBox%
+    \else% 
+        \displace=\curCenter%
+        \advance \displace by -\newCenter%
+        \kernLowerBox%
+    \fi%
+%    \end{macrocode}
+% For |\ddotsDeduce|, move lower box right; for |\dotsdDeduce|, move
+% upper box right; then set |\curCenter| to align with horizontal center
+% of dots.
+%    \begin{macrocode}
+    \ifnum\DiagCorrection<0%
+        \displace=-\DiagCorrection
+        \kernLowerBox%
+    \else
+        \displace=\DiagCorrection
+        \kernUpperBox%
+    \fi%
+    \advance\curCenter by-.5\DiagCorrection
+%    \end{macrocode}
+% Now we draw the deduction.
+%    \begin{macrocode}
+    \buildDeduce%
+%    \end{macrocode}
+% Put the deduction and labels into a box.
+%    \begin{macrocode}
+    \buildScoreLabels%
+%    \end{macrocode}
+% Put everything into a new box and compute the dimensions for the
+% next |\Deduce| or |\XxxxInf|.
+%    \begin{macrocode}
+    \ifx\rootAtBottomFlag\myTrue%
+        \buildRootBottom%
+    \else%
+        \buildRootTop%
+    \fi%
+    \global \curScoreStart=\newScoreStart%
+    \global \curScoreEnd=\newScoreEnd%
+    \global \curCenter=\newCenter%
+}
+%    \end{macrocode}
+% |\buildDeduce| does for |\DeduceX| what |\buildInf| does for
+% |\XxxInf|: put the deduction bit (dots) into a box and set the
+% dimensions properly.
+%    \begin{macrocode}
+
+\def\buildDeduce{%
+    \global\setbox \myBoxD =%
+        \hbox{\fDeduce}%
+    \displace = \wd\myBoxD % find width of vdots
+%    \end{macrocode}
+% set start and end of current score to left and right of the box
+% holding the deduction.
+%    \begin{macrocode}
+    \global\curScoreStart = \curCenter% 
+    \global\advance\curScoreStart by -.5\displace%
+    \global\curScoreEnd = \curCenter% 
+    \global\advance\curScoreEnd by .5\displace%
+    \global\advance\curScoreStart by\CenterCorrection
+    \global\advance\curScoreEnd by\CenterCorrection
+}
+%    \end{macrocode}
+% \subsection{Line Labels}
+% 
+% |\LeftLineLabel| and |\RightLineLabel| set the label to place to the
+% left or right, respectively, of the conclusion of the next |\Axiom|,
+% |\XxxInf| or |\Deduce| command. They are aligned with the text
+% produced by |\LeftLabel| and |\RightLabel| (i.e., the distance to
+% the line is $|\ScoreOverhang| + |\labelSpacing|$.
+%    \begin{macrocode}
+
+\def\LeftLineLabel#1{%
+  \global\def\displayLeftLineLabel{%
+    {#1\hskip\labelSpacing}}
+  \ignorespaces}
+
+\def\RightLineLabel#1{%
+  \global\def\displayRightLineLabel{%
+    {\hskip\labelSpacing #1}}
+  \ignorespaces}
+
+\global\let\displayLeftLineLabel\relax
+\global\let\displayRightLineLabel\relax
+%    \end{macrocode}
+%
+% \subsection{Subproof Labels}
+% Sometimes you'd like to lable entire subproofs.  This is done with
+% commands |\LeftSubproofLabel| and |\RightSubproofLabel|.
+%    \begin{macrocode}
+
+\def\LeftSubproofLabel#1{%
+  \global\setbox\curBox =
+  \hbox{\vbox to \ht\curBox{%
+      \vfil
+      \llap{#1$\left\{\vrule height .5\ht\curBox width 0pt\right.$}%
+      \vfil}\box\curBox}%
+}
+
+\def\RightSubproofLabel#1{%
+  \displace=\ht\curBox
+  \global\setbox\curBox =
+  \hbox{\box\curBox\vbox to \displace{%
+      \vfil
+      \rlap{$\left.\vrule height .5\displace width 0pt\right\}$#1}%
+      \vfil}}%
+}
+%    \end{macrocode}
+% \subsection{Patched commands from \textsf{bussproofs}}
+%
+% Some commands from \textsf{bussproofs.sty} have to be redefined to include
+% |bussproofs-extra| functionality. Added/changed lines are indicated by a
+% |%bpextra| comment
+%    \begin{macrocode}
+\def\resetInferenceDefaults{%
+    \global\def\theHypSeparation{\defaultHypSeparation}%
+    \global\setbox\myBoxLL=\hbox{\defaultLeftLabel}%
+    \global\setbox\myBoxRL=\hbox{\defaultRightLabel}%
+    \global\def\buildScore{\alwaysBuildScore}%
+    \global\def\theScoreFiller{\alwaysScoreFiller}%
+    % reset line labels to nothing %bpextra
+    \global\let\displayLeftLineLabel\relax %bpextra
+    \global\let\displayRightLineLabel\relax %bpextra
+    % reset to defaul deduce style %bpextra
+    \alwaysDeduce %bpextra
+    \gdef\hypKernAmt{0pt}% Restore to zero kerning.
+}
+
+\def\Axiom$#1\fCenter#2${%
+    % Get level and correct names set.
+    \prepAxiom%
+    % Define the boxes
+    % bpextra -- add line labels
+    \setbox\myBoxA=\hbox{$\mathord{#1}\fCenter\mathord{\relax}$}% 
+    \setbox\myBoxB=\hbox{$#2$}% %bpextra
+    \setbox\myBoxLLL=\hbox{\displayLeftLineLabel}% %bpextra
+    \setbox\myBoxRLL=\hbox{\displayRightLineLabel}% %bpextra
+    \global\setbox\curBox=%
+         \hbox{\unhcopy\myBoxLLL%bpextra
+         \hskip\ScoreOverhangLeft\relax
+         \unhcopy\myBoxA
+         \unhcopy\myBoxB
+         \hskip\ScoreOverhangRight
+         \unhcopy\myBoxRLL}%bpextra
+    % Set the relevant dimensions for the boxes
+    \global\curScoreStart=0pt \relax
+    \global\curScoreEnd=\wd\curBox \relax
+    \global\curCenter=\wd\myBoxA \relax %bpextra
+    \global\advance \curCenter by \ScoreOverhangLeft%
+    % bpextra adjust by dimensions of labels
+    \global\advance \curCenter by \wd\myBoxLLL%bpextra
+    \global\advance\curScoreStart by \wd\myBoxLLL%bpextra
+    \global\advance\curScoreEnd by -\wd\myBoxRLL%bpextra
+    % reset line labels to nothing %bpextra
+    \global\let\displayLeftLineLabel\relax %bpextra
+    \global\let\displayRightLineLabel\relax %bpextra
+    \ignorespaces
+}
+
+\def\AxiomC#1{      % Note argument not in math mode
+    % Get level and correct names set.
+    \prepAxiom%
+        % Define the box.
+    \setbox\myBoxA=\hbox{#1}%
+    \setbox\myBoxLLL=\hbox{\displayLeftLineLabel}% %bpextra
+    \setbox\myBoxRLL=\hbox{\displayRightLineLabel}% %bpextra
+    \global\setbox\curBox =%
+        \hbox{\unhcopy\myBoxLLL%bpextra
+            \hskip\ScoreOverhangLeft\relax%
+            \unhcopy\myBoxA
+            \hskip\ScoreOverhangRight\relax
+            \unhcopy\myBoxRLL}% %bpextra
+    % Set the relevant dimensions for the boxes
+        \global\curScoreStart=0pt \relax
+        \global\curScoreEnd=\wd\curBox \relax
+        \global\curCenter=.5\wd\myBoxA \relax %bpextra
+        \global\advance \curCenter by \ScoreOverhangLeft%
+    % bpextra adjust by dimensions of labels
+    \global\advance \curCenter by \wd\myBoxLLL%bpextra
+    \global\advance\curScoreStart by \wd\myBoxLLL%bpextra
+    \global\advance\curScoreEnd by -\wd\myBoxRLL%bpextra
+    % reset line labels to nothing %bpextra
+    \global\let\displayLeftLineLabel\relax %bpextra
+    \global\let\displayRightLineLabel\relax %bpextra
+    \ignorespaces
+}
+
+\def\buildConclusion#1#2{% Build lower sequent w/ center at \fCenter position.
+    % Define the boxes
+        \setbox\myBoxA=\hbox{$\mathord{#1}\fCenter\mathord{\relax}$}% 
+        \setbox\myBoxB=\hbox{$#2$}% 
+        \setbox\myBoxLLL=\hbox{\displayLeftLineLabel}% %bpextra
+        \setbox\myBoxRLL=\hbox{\displayRightLineLabel}% %bpextra
+    % Put them together in \myBoxC
+    \setbox\myBoxC =%
+          \hbox{\unhcopy\myBoxLLL%bpextra
+          \hskip\ScoreOverhangLeft\relax%
+        \unhcopy\myBoxA\unhcopy\myBoxB
+        \hskip\ScoreOverhangRight
+        \unhcopy\myBoxRLL}% %bpextra
+    % Calculate the center of the \myBoxC string.
+    \newScoreStart=0pt \relax%
+    \newCenter=\wd\myBoxA \relax%
+    \advance \newCenter by \ScoreOverhangLeft%
+    \newScoreEnd=\wd\myBoxC%
+    % bpextra adjust by dimensions of labels
+    \global\advance\newCenter by \wd\myBoxLLL%bpextra
+    \global\advance\newScoreStart by \wd\myBoxLLL%bpextra
+    \global\advance\newScoreEnd by -\wd\myBoxRLL%bpextra
+    % reset line labels to nothing %bpextra
+    \global\let\displayLeftLineLabel\relax %bpextra
+    \global\let\displayRightLineLabel\relax %bpextra
+}
+
+\def\buildConclusionC#1{% Build lower sequent w/o \fCenter present.
+        % Define the box.
+    \setbox\myBoxA=\hbox{#1}%
+    \setbox\myBoxLLL=\hbox{\displayLeftLineLabel}% %bpextra
+    \setbox\myBoxRLL=\hbox{\displayRightLineLabel}% %bpextra
+\setbox\myBoxC =%
+        \hbox{\unhcopy\myBoxLLL%bpextra
+            \hskip\ScoreOverhangLeft\relax%
+            \unhcopy\myBoxA
+            \hskip\ScoreOverhangRight
+            \unhcopy\myBoxRLL}%bpextra
+    % Calculate kerning to line up centers
+    \newScoreStart=0pt \relax%
+    \newCenter=.5\wd\myBoxA \relax% bpextra
+    \newScoreEnd=\wd\myBoxC%
+        \advance \newCenter by \ScoreOverhangLeft%
+    % bpextra adjust by dimensions of labels
+    \global\advance\newCenter by \wd\myBoxLLL%bpextra
+    \global\advance\newScoreStart by \wd\myBoxLLL%bpextra
+    \global\advance\newScoreEnd by -\wd\myBoxRLL%bpextra
+    % reset line labels to nothing %bpextra
+    \global\let\displayLeftLineLabel\relax %bpextra
+    \global\let\displayRightLineLabel\relax %bpextra
+}
+%    \end{macrocode}
+% \Finale
+% \PrintChanges
+\endinput
diff --git a/macros/latex/contrib/bussproofs-extra/bussproofs-extra.ins b/macros/latex/contrib/bussproofs-extra/bussproofs-extra.ins
new file mode 100644
index 0000000000..e511feff73
--- /dev/null
+++ b/macros/latex/contrib/bussproofs-extra/bussproofs-extra.ins
@@ -0,0 +1,57 @@
+%%
+%% Copyright (C) 2019 by Richard Zach <rzach@ucalgary.ca>
+%%
+%% This file may be distributed and/or modified under the conditions of
+%% the LaTeX Project Public License, either version 1.2 of this license
+%% or (at your option) any later version.  The latest version of this
+%% license is in:
+%% 
+%%    http://www.latex-project.org/lppl.txt
+%% 
+%% and version 1.2 or later is part of all distributions of LaTeX version
+%% 1999/12/01 or later.
+%%
+
+\input docstrip.tex
+\keepsilent
+
+\usedir{tex/latex/bussproofs-extra}
+
+\preamble
+
+This is a generated file.
+
+Copyright (C) 2019 by Richard Zach <rzach@ucalgary.ca>
+
+This file may be distributed and/or modified under the conditions of
+the LaTeX Project Public License, either version 1.3 of this license
+or (at your option) any later version.  The latest version of this
+license is in:
+
+   http://www.latex-project.org/lppl.txt
+
+and version 1.3 or later is part of all distributions of LaTeX version
+1999/12/01 or later.
+
+\endpreamble
+
+\generate{\file{bussproofs-extra.sty}{\from{bussproofs-extra.dtx}{package}}}
+
+\obeyspaces
+\Msg{*************************************************************}
+\Msg{*                                                           *}
+\Msg{* To finish the installation you have to move the following *}
+\Msg{* file into a directory searched by TeX:                    *}
+\Msg{*                                                           *}
+\Msg{*     bussproofs-extra.sty                                  *}
+\Msg{*                                                           *}
+\Msg{* To produce the documentation run the file bpextra.dtx     *}
+\Msg{* through LaTeX, and then                                   *}
+\Msg{* makeindex -s gglo.ist -o bussproofs-extra.gls bussproofs-extra.glo *}
+\Msg{* Then run LaTeX on bussproofs-extra.dtx again              *}
+\Msg{*                                                           *}
+\Msg{* Happy TeXing!                                             *}
+\Msg{*                                                           *}
+\Msg{*************************************************************}
+
+\endbatchfile
diff --git a/macros/latex/contrib/bussproofs-extra/bussproofs-extra.pdf b/macros/latex/contrib/bussproofs-extra/bussproofs-extra.pdf
new file mode 100644
index 0000000000..d20f69d4fa
--- /dev/null
+++ b/macros/latex/contrib/bussproofs-extra/bussproofs-extra.pdf