summaryrefslogtreecommitdiff
path: root/Master/texmf-dist/doc/latex/prftree/prftreedoc.tex
diff options
context:
space:
mode:
Diffstat (limited to 'Master/texmf-dist/doc/latex/prftree/prftreedoc.tex')
-rw-r--r--Master/texmf-dist/doc/latex/prftree/prftreedoc.tex69
1 files changed, 60 insertions, 9 deletions
diff --git a/Master/texmf-dist/doc/latex/prftree/prftreedoc.tex b/Master/texmf-dist/doc/latex/prftree/prftreedoc.tex
index 9db4c1f9e90..1fe8d227c6c 100644
--- a/Master/texmf-dist/doc/latex/prftree/prftreedoc.tex
+++ b/Master/texmf-dist/doc/latex/prftree/prftreedoc.tex
@@ -115,10 +115,12 @@ Assumptions are optional and there may be any number of them. Each
assumption may contain a proof tree, which is typeset independently:
the order allows to use indentation to help reading the source. The
conclusion is mandatory, and it is supposed to be a
-formula. Assumptions and the conclusion are typeset in a display style
-math environment. Options control the way the proof is generated: in
-the example, the \verb|r| option has been used to signal that the
-first argument of \verb|\prftree| is the name of the inference rule.
+formula.
+
+Assumptions and the conclusion are typeset in a display style math
+environment. Options control the way the proof is generated: in the
+example, the \verb|r| option has been used to signal that the first
+argument of \verb|\prftree| is the name of the inference rule.
The available options are:
\begin{itemize}
@@ -294,7 +296,7 @@ constructed:
on the left and on the right the proof line so that it is slightly
longer than the largest between the conclusion and the list of
(direct) assumptions;
-\item\ \verb|\prflinethickness| (default 0.2pt): the thickness of the
+\item\ \verb|\prflinethickness| (default 0.12ex): the thickness of the
proof line;
\item\ \verb|\prfemptylinethickness| (default 4 times the line
thickness): in the rare case when the line is empty, but there are
@@ -304,15 +306,15 @@ constructed:
proof line and the rule name;
\item\ \verb|\prflabelskip| (default 0.2em): the space between the
proof label and the proof line;
-\item\ \verb|\prfinterspace| (default .6em): the space between two
+\item\ \verb|\prfinterspace| (default .8em): the space between two
subsequent assumptions in the assumption list;
-\item\ \verb|\prfdoublelineinterspace| (default 1.2pt): the space
+\item\ \verb|\prfdoublelineinterspace| (default 0.06ex): the space
between the two lines of a double line.
\end{itemize}
For example,
\begin{displaymath}
- \prflinepadafter=.7ex
+ \prflinepadafter=0ex
\prftree[r]{$\supset$I}
{\prftree[r]{$\supset$I}
{\prftree[r]{$\supset$E}
@@ -324,7 +326,7 @@ For example,
\end{displaymath}
is typeset by
\begin{verbatim}
- \prflinepadafter=.7ex
+ \prflinepadafter=0ex
\prftree[r]{$\supset$I}
{\prftree[r]{$\supset$I}
{\prftree[r]{$\supset$E}
@@ -704,6 +706,7 @@ The generation of labels is controlled by the option value:
defined. This is used to generate a labelled assumption sharing the
label with another one, which declares the value and the format.
\end{itemize}
+
Except for \textbf{l} and \textbf{label}, all the options are used to
format the anchor following the standard \LaTeX{} way available for
counters. No multiple options are allowed.
@@ -737,8 +740,10 @@ may indicate that a label is reused when it should not.
The same example can be used to show how the other options work:
\begin{displaymath}
+ \renewcommand{\arraystretch}{6}
\begin{array}{@{}ccc@{}}
\begin{prfenv}
+ \prfinterspace=.6em
\prfsummarystyle=2
\prftree[r]{$\vee\mathrm{E}_{\prfref<assum:orEn>}$}
{\prfsummary{\Gamma}{A \vee B}}
@@ -749,6 +754,7 @@ The same example can be used to show how the other options work:
{C}
\end{prfenv} &
\begin{prfenv}
+ \prfinterspace=.6em
\prfsummarystyle=2
\prftree[r]{$\vee\mathrm{E}_{\prfref<assum:orEr>}$}
{\prfsummary{\Gamma}{A \vee B}}
@@ -759,6 +765,7 @@ The same example can be used to show how the other options work:
{C}
\end{prfenv} &
\begin{prfenv}
+ \prfinterspace=.6em
\prfsummarystyle=2
\prftree[r]{$\vee\mathrm{E}_{\prfref<assum:orER>}$}
{\prfsummary{\Gamma}{A \vee B}}
@@ -769,6 +776,7 @@ The same example can be used to show how the other options work:
{C}
\end{prfenv} \\
\begin{prfenv}
+ \prfinterspace=.6em
\prfsummarystyle=2
\prftree[r]{$\vee\mathrm{E}_{\prfref<assum:orEa>}$}
{\prfsummary{\Gamma}{A \vee B}}
@@ -779,6 +787,7 @@ The same example can be used to show how the other options work:
{C}
\end{prfenv} &
\begin{prfenv}
+ \prfinterspace=.6em
\prfsummarystyle=2
\prftree[r]{$\vee\mathrm{E}_{\prfref<assum:orEA>}$}
{\prfsummary{\Gamma}{A \vee B}}
@@ -789,6 +798,7 @@ The same example can be used to show how the other options work:
{C}
\end{prfenv} &
\begin{prfenv}
+ \prfinterspace=.6em
\prfsummarystyle=2
\prftree[r]{$\vee\mathrm{E}_{\prfref<assum:orEf>}$}
{\prfsummary{\Gamma}{A \vee B}}
@@ -806,6 +816,7 @@ are:
\begin{displaymath}
\begin{array}{ccc}
\begin{prfenv}
+ \prfinterspace=.6em
\prfboundedstyle=0
\prfsummarystyle=4
\prftree[r]{$\vee\mathrm{E}_{\prfref<assum:AorE>}$}
@@ -817,6 +828,7 @@ are:
{C}
\end{prfenv} &
\begin{prfenv}
+ \prfinterspace=.6em
\prfboundedstyle=1
\prfsummarystyle=4
\prftree[r]{$\vee\mathrm{E}_{\prfref<assum:BorE>}$}
@@ -828,6 +840,7 @@ are:
{C}
\end{prfenv} &
\begin{prfenv}
+ \prfinterspace=.6em
\prfboundedstyle=2
\prfsummarystyle=4
\prftree[r]{$\vee\mathrm{E}_{\prfref<assum:CorE>}$}
@@ -1327,6 +1340,7 @@ the previous sections for the description of the features.\vspace{2ex}
The disjunction elimination rule, with various line options:
\begin{displaymath}
+ \renewcommand{\arraystretch}{3.7}
\begin{array}{@{}ccc@{}}
{\prfsummarystyle=1
\prftree{\prfsummary{\Gamma}{A \vee B}}
@@ -1639,6 +1653,38 @@ shrink a large proof to fit the page length:
% -------------------------------------
\clearpage
+\section{Fonts}\label{sec:fonts}
+The package works with any font. It uses the current math fonts for
+typesetting proofs, while it uses the current text font to typeset
+labels and rule names.
+
+Care has been taken to ensure that the various dimensions and
+parameters in Section~\ref{sec:parameters} are relative to the current
+font, that is, technically, they are expressed with units \texttt{ex}
+for vertical lengths, and \texttt{em} for horizontal lengths. Dashes
+are \TeX\ rules with thickness \verb|\prflinethickness|.
+
+For unknown reasons, the \texttt{fontenc} package modifies slightly
+the values for \texttt{ex} and \texttt{em}, thus the graphical
+appearance of proof trees may vary when comparing the results obtained
+by compiling with and without this package.
+
+In most cases, the graphical appearance of proofs is acceptable, even
+changing font and size. But using fonts whose body is particularly
+heavy, may result in proof lines which are too thin. In this case, the
+user of the package should increment the value of
+\verb|\prflinethickness|.
+
+The package, up to version 1.5, was designed to work with the Computer
+Modern family of fonts. It worked also with other fonts, without any
+major problem, but, as kindly signalled by D{\'e}mi Nollet at ENS Lyon
+and universit{\'e} Paris-Diderot, dashed and dotted lines do not
+behave correctly, as dashes overlap. Please, update to the latest
+version of the package if you plan to use fonts different from
+Computer Modern.
+
+% -------------------------------------
+\clearpage
\section{Internals}\label{sec:internals}
A proof tree is typeset as a \TeX{} box in horizontal mode. This means
that wherever a character can stay, so does a proof: in principle,
@@ -1780,4 +1826,9 @@ of this feature has been postponed to a remote future, or to the will
of a real \TeX{} magician.
\vfill
+Although the package has been tested for a long time, by now, it is
+possible that a few bugs are still present. To signal a bug, please,
+write an email to the author (see below), possibly attaching a sample
+document which exhibit the misbehaviour, to help tracking and fixing.
+\vfill
\end{document}