# HG changeset patch
# User wenzelm
# Date 926342209 -7200
# Node ID 13293a7d4a57ee24a403441ae2b02a5d21d678a9
# Parent  2d56911d732999ff7367ac4709563b162a99ffe9
pdf setup;

diff -r 2d56911d7329 -r 13293a7d4a57 doc-src/Ref/Makefile
--- a/doc-src/Ref/Makefile	Fri May 07 17:50:43 1999 +0200
+++ b/doc-src/Ref/Makefile	Mon May 10 15:16:49 1999 +0200
@@ -29,3 +29,17 @@
 	$(LATEX) $(NAME)
 	$(SEDINDEX) $(NAME)
 	$(LATEX) $(NAME)
+
+
+pdf: $(NAME).pdf
+
+$(NAME).pdf: $(FILES) isabelle.pdf
+	touch $(NAME).ind
+	$(PDFLATEX) $(NAME)
+	$(RAIL) $(NAME)
+	$(BIBTEX) $(NAME)
+	$(PDFLATEX) $(NAME)
+	$(PDFLATEX) $(NAME)
+	$(SEDINDEX) $(NAME)
+	$(FIXBOOKMARKS) $(NAME).out
+	$(PDFLATEX) $(NAME)
diff -r 2d56911d7329 -r 13293a7d4a57 doc-src/Ref/introduction.tex
--- a/doc-src/Ref/introduction.tex	Fri May 07 17:50:43 1999 +0200
+++ b/doc-src/Ref/introduction.tex	Mon May 10 15:16:49 1999 +0200
@@ -294,7 +294,7 @@
 \end{ttdescription}
 
 
-\subsection{$\eta$-contraction before printing}
+\subsection{Eta-contraction before printing}
 \begin{ttbox} 
 eta_contract: bool ref \hfill{\bf initially false}
 \end{ttbox}
diff -r 2d56911d7329 -r 13293a7d4a57 doc-src/Ref/ref.tex
--- a/doc-src/Ref/ref.tex	Fri May 07 17:50:43 1999 +0200
+++ b/doc-src/Ref/ref.tex	Mon May 10 15:16:49 1999 +0200
@@ -1,5 +1,5 @@
 \documentclass[12pt]{report}
-\usepackage{graphicx,a4,../iman,../extra,../proof,../rail,../pdfsetup}
+\usepackage{url,graphicx,a4,../iman,../extra,../proof,../rail,../pdfsetup}
 
 %% $Id$
 %%\includeonly{}
diff -r 2d56911d7329 -r 13293a7d4a57 doc-src/Ref/substitution.tex
--- a/doc-src/Ref/substitution.tex	Fri May 07 17:50:43 1999 +0200
+++ b/doc-src/Ref/substitution.tex	Mon May 10 15:16:49 1999 +0200
@@ -113,7 +113,7 @@
 insert the atomic premises as object-level assumptions.
 
 
-\section{Setting up {\tt hyp_subst_tac}} 
+\section{Setting up the package} 
 Many Isabelle object-logics, such as \texttt{FOL}, \texttt{HOL} and their
 descendants, come with \texttt{hyp_subst_tac} already defined.  A few others,
 such as \texttt{CTT}, do not support this tactic because they lack the
diff -r 2d56911d7329 -r 13293a7d4a57 doc-src/Ref/syntax.tex
--- a/doc-src/Ref/syntax.tex	Fri May 07 17:50:43 1999 +0200
+++ b/doc-src/Ref/syntax.tex	Mon May 10 15:16:49 1999 +0200
@@ -93,7 +93,7 @@
 constructor \ttindex{Bound}).
 
 
-\section{Transforming parse trees to \AST{}s}\label{sec:astofpt}
+\section{Transforming parse trees to ASTs}\label{sec:astofpt}
 \index{ASTs!made from parse trees}
 \newcommand\astofpt[1]{\lbrakk#1\rbrakk}
 
@@ -181,7 +181,7 @@
 output of {\tt print_syntax} under {\tt parse_ast_translation}.
 
 
-\section{Transforming \AST{}s to terms}\label{sec:termofast}
+\section{Transforming ASTs to terms}\label{sec:termofast}
 \index{terms!made from ASTs}
 \newcommand\termofast[1]{\lbrakk#1\rbrakk}
 
diff -r 2d56911d7329 -r 13293a7d4a57 doc-src/Ref/tactic.tex
--- a/doc-src/Ref/tactic.tex	Fri May 07 17:50:43 1999 +0200
+++ b/doc-src/Ref/tactic.tex	Mon May 10 15:16:49 1999 +0200
@@ -571,7 +571,7 @@
 Do not consider using the primitives discussed in this section unless you
 really need to code tactics from scratch.
 
-\subsection{Operations on type {\tt tactic}}
+\subsection{Operations on tactics}
 \index{tactics!primitives for coding} A tactic maps theorems to sequences of
 theorems.  The type constructor for sequences (lazy lists) is called
 \mltydx{Seq.seq}.  To simplify the types of tactics and tacticals,