2 files changed, 106 insertions, 0 deletions
diff --git a/Master/texmf-dist/doc/latex/lkproof/lkproof-doc.pdf b/Master/texmf-dist/doc/latex/lkproof/lkproof-doc.pdf
new file mode 100644
index 00000000000..56afe708b6a
--- /dev/null
+++ b/Master/texmf-dist/doc/latex/lkproof/lkproof-doc.pdf
diff --git a/Master/texmf-dist/doc/latex/lkproof/lkproof-doc.tex b/Master/texmf-dist/doc/latex/lkproof/lkproof-doc.tex
new file mode 100644
index 00000000000..7a134ab413f
--- /dev/null
+++ b/Master/texmf-dist/doc/latex/lkproof/lkproof-doc.tex
@@ -0,0 +1,106 @@
+\documentclass[pagesize=auto, fontsize=12pt, DIV=9, parskip=half]{scrartcl}
+
+\usepackage{fixltx2e}
+\usepackage{etex}
+\usepackage{lmodern}
+\usepackage[T1]{fontenc}
+\usepackage{textcomp}
+\usepackage[svgnames]{xcolor}
+\usepackage{proof}
+\usepackage{microtype}
+\usepackage{hyperref}
+
+\newcommand*{\mail}[1]{\href{mailto:#1}{\texttt{#1}}}
+\newcommand*{\pkg}[1]{\textsf{#1}}
+\newcommand*{\cs}[1]{\texttt{\textbackslash#1}}
+\makeatletter
+\newcommand*{\cmd}[1]{\cs{\expandafter\@gobble\string#1}}
+\makeatother
+\newcommand*{\opt}[1]{\texttt{#1}}
+\newcommand*{\meta}[1]{\textlangle\textsl{#1}\textrangle}
+\newcommand*{\marg}[1]{\texttt{\{}\meta{#1}\texttt{\}}}
+\newcommand*{\oarg}[1]{\texttt{[}\meta{#1}\texttt{]}}
+
+\addtokomafont{title}{\rmfamily}
+\addtokomafont{descriptionlabel}{\mdseries}
+
+\title{The \pkg{proof} package\thanks{This manual corresponds to \pkg{proof.sty}~v3.1 (for both \LaTeX\,2.09 and \LaTeXe), dated~Nov 24, 2005.}}
+\subtitle{Proof figure macros}
+\author{Makoto Tatsuta\thanks{\mail{tatsuta@nii.ac.jp}}}
+\date{Nov 24, 2005}
+
+
+\begin{document}
+
+\righthyphenmin=2
+
+\maketitle
+
+\section{Usage:}
+
+In \cmd{\documentstyle}, specify an optional style `\opt{proof}', say,\\
+\verb+\documentstyle[proof]{article}+.
+
+The following macros are available:
+
+In all the following macros, all the arguments such as
+\meta{Lowers} and \meta{Uppers} are processed in math mode.
+%
+\begin{description}
+\item[\cmd{\infer}\marg{Lower}\marg{Uppers}]
+  draws an inference.
+
+  Use \verb+&+ in \meta{Uppers} to delimit upper formulae.
+  \meta{Uppers} consists more than 0 formulae.
+
+  \cmd{\infer} returns \verb+\hbox{ ... }+ or \verb+\vbox{ ... }+ and
+  sets \cmd{\@LeftOffset} and \cmd{\@RightOffset} globally.
+  
+\item[\cmd{\infer}\oarg{Label}\marg{Lower}\marg{Uppers}]
+  draws an inference labeled with~\meta{Label}.
+
+\item[\cmd{\infer*}\marg{Lower}\marg{Uppers}]
+  draws a many step deduction.
+
+\item[\cmd{\infer*}\oarg{Label}\marg{Lower}\marg{Uppers}]
+  draws a many step deduction labeled with~\meta{Label}.
+
+\item[\cmd{\infer=}\marg{Lower}\marg{Uppers}]
+  draws a double-ruled deduction.
+
+\item[\cmd{\infer=}\oarg{Label}\marg{Lower}\marg{Uppers}]
+  \begingroup
+  \spaceskip=\fontdimen2\font plus \fontdimen3\font minus 1.2\fontdimen4\font
+  draws a double-ruled deduction labeled with~\meta{Label}.
+  \endgroup
+
+\item[\cmd{\deduce}\marg{Lower}\marg{Uppers}]
+  draws an inference without a rule.
+
+\item[\cmd{\deduce}\oarg{Proof}\marg{Lower}\marg{Uppers}]
+  draws a many step deduction with a proof~name.  
+\end{description}
+
+
+\section{Example:}
+
+If you want to write
+
+\medskip
+\infer{E}{
+  A
+  &
+  \infer{D}{B & C}
+}
+
+use
+%
+\begin{verbatim}
+\infer{E}{
+  A
+  &
+  \infer{D}{B & C}
+}
+\end{verbatim}
+
+\end{document}