\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}