1.1 --- a/doc-src/Ref/Makefile	Fri May 07 17:50:43 1999 +0200
     1.2 +++ b/doc-src/Ref/Makefile	Mon May 10 15:16:49 1999 +0200
     1.3 @@ -29,3 +29,17 @@
     1.4  	$(LATEX) $(NAME)
     1.5  	$(SEDINDEX) $(NAME)
     1.6  	$(LATEX) $(NAME)
     1.7 +
     1.8 +
     1.9 +pdf: $(NAME).pdf
    1.10 +
    1.11 +$(NAME).pdf: $(FILES) isabelle.pdf
    1.12 +	touch $(NAME).ind
    1.13 +	$(PDFLATEX) $(NAME)
    1.14 +	$(RAIL) $(NAME)
    1.15 +	$(BIBTEX) $(NAME)
    1.16 +	$(PDFLATEX) $(NAME)
    1.17 +	$(PDFLATEX) $(NAME)
    1.18 +	$(SEDINDEX) $(NAME)
    1.19 +	$(FIXBOOKMARKS) $(NAME).out
    1.20 +	$(PDFLATEX) $(NAME)

     2.1 --- a/doc-src/Ref/introduction.tex	Fri May 07 17:50:43 1999 +0200
     2.2 +++ b/doc-src/Ref/introduction.tex	Mon May 10 15:16:49 1999 +0200
     2.3 @@ -294,7 +294,7 @@
     2.4  \end{ttdescription}
     2.5  
     2.6  
     2.7 -\subsection{$\eta$-contraction before printing}
     2.8 +\subsection{Eta-contraction before printing}
     2.9  \begin{ttbox} 
    2.10  eta_contract: bool ref \hfill{\bf initially false}
    2.11  \end{ttbox}

     3.1 --- a/doc-src/Ref/ref.tex	Fri May 07 17:50:43 1999 +0200
     3.2 +++ b/doc-src/Ref/ref.tex	Mon May 10 15:16:49 1999 +0200
     3.3 @@ -1,5 +1,5 @@
     3.4  \documentclass[12pt]{report}
     3.5 -\usepackage{graphicx,a4,../iman,../extra,../proof,../rail,../pdfsetup}
     3.6 +\usepackage{url,graphicx,a4,../iman,../extra,../proof,../rail,../pdfsetup}
     3.7  
     3.8  %% $Id$
     3.9  %%\includeonly{}

     4.1 --- a/doc-src/Ref/substitution.tex	Fri May 07 17:50:43 1999 +0200
     4.2 +++ b/doc-src/Ref/substitution.tex	Mon May 10 15:16:49 1999 +0200
     4.3 @@ -113,7 +113,7 @@
     4.4  insert the atomic premises as object-level assumptions.
     4.5  
     4.6  
     4.7 -\section{Setting up {\tt hyp_subst_tac}} 
     4.8 +\section{Setting up the package} 
     4.9  Many Isabelle object-logics, such as \texttt{FOL}, \texttt{HOL} and their
    4.10  descendants, come with \texttt{hyp_subst_tac} already defined.  A few others,
    4.11  such as \texttt{CTT}, do not support this tactic because they lack the

     5.1 --- a/doc-src/Ref/syntax.tex	Fri May 07 17:50:43 1999 +0200
     5.2 +++ b/doc-src/Ref/syntax.tex	Mon May 10 15:16:49 1999 +0200
     5.3 @@ -93,7 +93,7 @@
     5.4  constructor \ttindex{Bound}).
     5.5  
     5.6  
     5.7 -\section{Transforming parse trees to \AST{}s}\label{sec:astofpt}
     5.8 +\section{Transforming parse trees to ASTs}\label{sec:astofpt}
     5.9  \index{ASTs!made from parse trees}
    5.10  \newcommand\astofpt[1]{\lbrakk#1\rbrakk}
    5.11  
    5.12 @@ -181,7 +181,7 @@
    5.13  output of {\tt print_syntax} under {\tt parse_ast_translation}.
    5.14  
    5.15  
    5.16 -\section{Transforming \AST{}s to terms}\label{sec:termofast}
    5.17 +\section{Transforming ASTs to terms}\label{sec:termofast}
    5.18  \index{terms!made from ASTs}
    5.19  \newcommand\termofast[1]{\lbrakk#1\rbrakk}
    5.20  

     6.1 --- a/doc-src/Ref/tactic.tex	Fri May 07 17:50:43 1999 +0200
     6.2 +++ b/doc-src/Ref/tactic.tex	Mon May 10 15:16:49 1999 +0200
     6.3 @@ -571,7 +571,7 @@
     6.4  Do not consider using the primitives discussed in this section unless you
     6.5  really need to code tactics from scratch.
     6.6  
     6.7 -\subsection{Operations on type {\tt tactic}}
     6.8 +\subsection{Operations on tactics}
     6.9  \index{tactics!primitives for coding} A tactic maps theorems to sequences of
    6.10  theorems.  The type constructor for sequences (lazy lists) is called
    6.11  \mltydx{Seq.seq}.  To simplify the types of tactics and tacticals,