diff options
Diffstat (limited to 'macros/latex/contrib/lkproof/lkproof-doc.tex')
-rw-r--r-- | macros/latex/contrib/lkproof/lkproof-doc.tex | 106 |
1 files changed, 106 insertions, 0 deletions
diff --git a/macros/latex/contrib/lkproof/lkproof-doc.tex b/macros/latex/contrib/lkproof/lkproof-doc.tex new file mode 100644 index 0000000000..7a134ab413 --- /dev/null +++ b/macros/latex/contrib/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} |