summaryrefslogtreecommitdiff
path: root/macros/latex/contrib/lkproof/lkproof-doc.tex
blob: 7a134ab413ff1fd9145f9d500a390b55054b70ad (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
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}