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