# HG changeset patch
# User wenzelm
# Date 926342790 -7200
# Node ID fc991461c7b9f4bd211bad92bdb9ba80b9eefe17
# Parent  010dfaf75064094a862f991c7119d297f10715d2
pdf setup;

diff -r 010dfaf75064 -r fc991461c7b9 doc-src/HOL/HOL.tex
--- 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
diff -r 010dfaf75064 -r fc991461c7b9 doc-src/HOL/Makefile
--- 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)
diff -r 010dfaf75064 -r fc991461c7b9 doc-src/HOL/logics-HOL.tex
--- 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}