--- 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)
--- 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}
--- 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{}
--- 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
--- 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}
--- 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,