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
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
|
% =====================================================================
% Macros for typesetting hol reference manual entries
% =====================================================================
\newlength{\minipagewidth}
\setlength{\minipagewidth}{\textwidth}
\addtolength{\minipagewidth}{-1.10em}
% ---------------------------------------------------------------------
% boolean flag for verbose printing of reference manual typesetting
% ---------------------------------------------------------------------
\newif\ifverboseref
\verbosereffalse % don't be verbose
% ---------------------------------------------------------------------
% Macro for generating right-hand page running titles.
% ---------------------------------------------------------------------
\makeatletter
\def\mkhead{\futurelet\@t\chsize}
\def\chsize#1.{\ifx a\@t \markright{{\protect\bf #1}}\else
\ifx b\@t \markright{{\protect\bf #1}}\else
\ifx c\@t \markright{{\protect\bf #1}}\else
\ifx d\@t \markright{{\protect\bf #1}}\else
\ifx e\@t \markright{{\protect\bf #1}}\else
\ifx f\@t \markright{{\protect\bf #1}}\else
\ifx g\@t \markright{{\protect\bf #1}}\else
\ifx h\@t \markright{{\protect\bf #1}}\else
\ifx i\@t \markright{{\protect\bf #1}}\else
\ifx j\@t \markright{{\protect\bf #1}}\else
\ifx k\@t \markright{{\protect\bf #1}}\else
\ifx l\@t \markright{{\protect\bf #1}}\else
\ifx m\@t \markright{{\protect\bf #1}}\else
\ifx n\@t \markright{{\protect\bf #1}}\else
\ifx o\@t \markright{{\protect\bf #1}}\else
\ifx p\@t \markright{{\protect\bf #1}}\else
\ifx q\@t \markright{{\protect\bf #1}}\else
\ifx r\@t \markright{{\protect\bf #1}}\else
\ifx s\@t \markright{{\protect\bf #1}}\else
\ifx t\@t \markright{{\protect\bf #1}}\else
\ifx u\@t \markright{{\protect\bf #1}}\else
\ifx v\@t \markright{{\protect\bf #1}}\else
\ifx w\@t \markright{{\protect\bf #1}}\else
\ifx z\@t \markright{{\protect\bf #1}}\else
\ifx y\@t \markright{{\protect\bf #1}}\else
\ifx z\@t \markright{{\protect\bf #1}}\else
\markright{{\protect\small\bf #1}}\fi
\fi\fi\fi\fi\fi\fi\fi\fi\fi\fi\fi\fi\fi\fi\fi
\fi\fi\fi\fi\fi\fi\fi\fi\fi\fi}
\makeatother
% ---------------------------------------------------------------------
% \DOC{<object>} : start a manual entry for <object>.
% ---------------------------------------------------------------------
\newcommand{\DOC}[1]%
{\bigskip
{\ifverboseref{\def\_{\string_}\typeout{Typesetting: #1}}\fi}
\bgroup\samepage % ended after \TYPE
\mkhead #1.
\begin{flushleft}
\begin{tabular}{|c|}\hline
\begin{minipage}{\minipagewidth}
\bigskip
{\def\_{\char'137}\LARGE\tt #1}
\bigskip
\end{minipage}\\ \hline
\end{tabular}
\end{flushleft}
\vskip10pt}
% ---------------------------------------------------------------------
% \setseps = set the spacing parameters for above and below displays
% ---------------------------------------------------------------------
\def\setseps{\partopsep=0mm\topsep=12pt plus2pt minus2pt}
% ---------------------------------------------------------------------
% flag for typesetting SEEALSO list
% ---------------------------------------------------------------------
\newif\ifseealso
\seealsofalse % start false.
% ---------------------------------------------------------------------
% \TYPE {<thing>} : {<type>}
% ---------------------------------------------------------------------
\def\TYPE{\noindent}
% ---------------------------------------------------------------------
% Commands for parts of a \DOC:
% \SYNOPSIS
% \DESCRIBE
% \FAILURE
% \EXAMPLE
% \USES
% \SEEALSO
% ---------------------------------------------------------------------
\newcommand\beforeskip{\vspace{12pt plus4pt minus4pt}}
\newcommand{\SYNOPSIS}%
{\beforeskip\leftline{\large\bf Synopsis}\nobreak\noindent}
\newcommand{\DESCRIBE}%
{\beforeskip\leftline{\large\bf Description}\nobreak\noindent}
\newcommand{\FAILURE}%
{\beforeskip\leftline{\large\bf Failure}\nobreak\noindent}
\newcommand{\EXAMPLE}%
{\beforeskip\leftline{\large\bf Example}\nobreak\noindent}
\newcommand{\USES}%
{\beforeskip\leftline{\large\bf Uses}\nobreak\noindent}
\newcommand{\COMMENTS}%
{\beforeskip\leftline{\large\bf Comments}\nobreak\noindent}
\newcommand{\SEEALSO}%
{\beforeskip\seealsotrue\leftline{\large\bf See also}\nobreak\noindent%
\bgroup\raggedright\small\tt\catcode`\_=12}
% ---------------------------------------------------------------------
% \ENDDOC = do nothing, but close off the group started by \SEEALSO
% ---------------------------------------------------------------------
\newcommand{\ENDDOC}{\ifseealso \egroup\seealsofalse \else \relax \fi}
% =====================================================================
% Commands for typesetting theorems
% =====================================================================
\makeatletter
% ---------------------------------------------------------------------
% define \@xboxverb<thing>\ENDTHEOREM to mean <thing>\ENDTHEOREM
% ---------------------------------------------------------------------
\begingroup \catcode `|=0 \catcode `[= 1
\catcode`]=2 \catcode `\{=12 \catcode `\}=12
\catcode`\\=12 |gdef|@xboxverb#1\ENDTHEOREM[#1|ENDTHEOREM]
|endgroup
% ---------------------------------------------------------------------
% \bboxverb<thing> = <thing> in a verbatim box 5mm from left margin
% ---------------------------------------------------------------------
\def\@boxverb{\bgroup\leftskip=5mm\parindent\z@
\parfillskip=\@flushglue\parskip\z@
\obeylines\small\tt \catcode``=13 \@noligs \let\do\@makeother \dospecials}
\def\boxverb{\@boxverb \frenchspacing\@vobeyspaces \@xboxverb}
% ---------------------------------------------------------------------
% \ENDTHEOREM just finishes off the group (and kick page if necessary)
% ---------------------------------------------------------------------
\def\ENDTHEOREM{\egroup\filbreak}
% ---------------------------------------------------------------------
% \THEOREM <name> <thy> ... \ENDTHEOREM = typeset a theorem
% ---------------------------------------------------------------------
\def\THEOREM #1 #2 {
\vspace{4mm plus2mm minus1mm}
\noindent {\def\_{{\char'137}}\small\tt #1}\quad({\small\tt #2}) \par \boxverb
}
\makeatother
% ---------------------------------------------------------------------
% The theory name \none = italic "none"
% ---------------------------------------------------------------------
\def\none{{\it none}}
|
