Merge pull request #262 from mathjax/v3.1-bussproofs

Documentation of the bussproofs package.

Author: dpvc

input/tex/extensions/bussproofs.rst

@@ -4,9 +4,46 @@
 bussproofs
 ##########
 
-The `bussproofs` extension defines ...
+The `bussproofs` extension implements the ``bussproofs`` style package from
+LaTeX. See the `Ctan page <https://www.ctan.org/pkg/bussproofs>`__ for
+more information and documentation of `bussproofs`.
 
-[description here]
+Note that there are a couple of important differences to the use of the actual
+package: Proofs always have to be in a `prooftree` environment, i.e., inference
+macros are only recognised if they are enclosed in `\begin{prooftree}` and
+`\end{prooftree}`. Consequently the `\DisplayProof` command is not necessary.
+
+Unlike in the LaTeX package, options for abbreviated inference rule macros do
+not have to be manually set. All abbreviated macros are directly available. Thus
+commands like `\BinaryInfC` and `\BIC` can be used immediately and
+interchangeably.
+
+
+For example
+
+.. code-block:: latex
+
+    \begin{prooftree}
+    \AxiomC{}
+    \RightLabel{Hyp$^{1}$}
+    \UnaryInfC{$P$}
+    \AXC{$P\to Q$}
+    \RL{$\to_E$}
+    \BIC{$Q^2$}
+    \AXC{$Q\to R$} 
+    \RL{$\to_E$} 
+    \BIC{$R$} 
+    \AXC{$Q$} 
+    \RL{Rit$^2$} 
+    \UIC{$Q$}
+    \RL{$\wedge_I$} 
+    \BIC{$Q\wedge R$} 
+    \RL{$\to_I$$^1$} 
+    \UIC{$P\to Q\wedge R$}
+    \end{prooftree}
+
+Also note that the `bussproofs` commands for sequent calculus derivations are
+not yet fully implemented.
 
 This extension is **not** loaded by the `autoload` extension is used.
 To load the `bussproofs` extension explicitly, add