--- a/doc-src/HOL/HOL.tex Mon May 10 15:17:14 1999 +0200
+++ b/doc-src/HOL/HOL.tex Mon May 10 15:26:30 1999 +0200
@@ -242,7 +242,7 @@
\end{warn}
-\subsection{The \sdx{let} and \sdx{case} constructions}
+\subsection{The let and case constructions}
Local abbreviations can be introduced by a \texttt{let} construct whose
syntax appears in Fig.\ts\ref{hol-grammar}. Internally it is translated into
the constant~\cdx{Let}. It can be expanded by rewriting with its
--- a/doc-src/HOL/Makefile Mon May 10 15:17:14 1999 +0200
+++ b/doc-src/HOL/Makefile Mon May 10 15:26:30 1999 +0200
@@ -27,3 +27,17 @@
$(LATEX) $(NAME)
$(SEDINDEX) $(NAME)
$(LATEX) $(NAME)
+
+
+pdf: $(NAME).pdf
+
+$(NAME).pdf: $(FILES) isabelle_hol.pdf
+ touch $(NAME).ind
+ $(PDFLATEX) $(NAME)
+ $(RAIL) $(NAME)
+ $(BIBTEX) $(NAME)
+ $(PDFLATEX) $(NAME)
+ $(PDFLATEX) $(NAME)
+ $(SEDINDEX) $(NAME)
+ $(FIXBOOKMARKS) $(NAME).out
+ $(PDFLATEX) $(NAME)
--- a/doc-src/HOL/logics-HOL.tex Mon May 10 15:17:14 1999 +0200
+++ b/doc-src/HOL/logics-HOL.tex Mon May 10 15:26:30 1999 +0200
@@ -14,7 +14,7 @@
%%% to index constants: \\tt \([a-zA-Z0-9][a-zA-Z0-9_]*\) \\cdx{\1}
%%% to deverbify: \\verb|\([^|]*\)| \\ttindex{\1}
-\title{\includegraphics[scale=0.5]{isabelle_hol.eps} \\[4ex]
+\title{\includegraphics[scale=0.5]{isabelle_hol} \\[4ex]
Isabelle's Logics: HOL}
\author{Tobias Nipkow\footnote
@@ -56,7 +56,7 @@
\end{abstract}
\pagenumbering{roman} \tableofcontents \clearfirst
-\include{../Logics/syntax}
+\input{../Logics/syntax}
\include{HOL}
\bibliographystyle{plain}
\bibliography{../manual}