# HG changeset patch
# User wenzelm
# Date 926351035 -7200
# Node ID 12ed4f748f7caba22f2a0c2cbdfa6082248a3f70
# Parent  c2511c9ea37e117c68ec3b54b3ce1c2fbd5a25c4
pdf setup;

diff -r c2511c9ea37e -r 12ed4f748f7c doc-src/Tutorial/Makefile
--- a/doc-src/Tutorial/Makefile	Mon May 10 17:07:19 1999 +0200
+++ b/doc-src/Tutorial/Makefile	Mon May 10 17:43:55 1999 +0200
@@ -5,7 +5,6 @@
 ## targets
 
 default: dvi
-dist: dvi
 
 
 ## dependencies
@@ -26,3 +25,15 @@
 	$(LATEX) $(NAME)
 	$(SEDINDEX) $(NAME)
 	$(LATEX) $(NAME)
+
+pdf: $(NAME).pdf
+
+$(NAME).pdf: $(FILES) isabelle_hol.pdf
+	touch $(NAME).ind
+	$(PDFLATEX) $(NAME)
+	$(BIBTEX) $(NAME)
+	$(PDFLATEX) $(NAME)
+	$(PDFLATEX) $(NAME)
+	$(SEDINDEX) $(NAME)
+	$(FIXBOOKMARKS) $(NAME).out
+	$(PDFLATEX) $(NAME)
diff -r c2511c9ea37e -r 12ed4f748f7c doc-src/Tutorial/basics.tex
--- a/doc-src/Tutorial/basics.tex	Mon May 10 17:07:19 1999 +0200
+++ b/doc-src/Tutorial/basics.tex	Mon May 10 17:43:55 1999 +0200
@@ -42,10 +42,14 @@
 automatically visible. To avoid name clashes, identifiers can be qualified by
 theory names as in \texttt{T.f} and \texttt{B.f}. HOL's theory library is
 available online at
-\begin{ttbox}
-http://www.cl.cam.ac.uk/Research/HVG/Isabelle/library/HOL/
-http://isabelle.in.tum.de/library/HOL/
-\end{ttbox}
+
+\begin{center}\small
+  \begin{tabular}{l}
+    \url{http://www.cl.cam.ac.uk/Research/HVG/Isabelle/library/} \\
+    \url{http://isabelle.in.tum.de/library/} \\
+  \end{tabular}
+\end{center}
+
 and is recommended browsing.
 \begin{warn}
   HOL contains a theory \ttindexbold{Main}, the union of all the basic
diff -r c2511c9ea37e -r 12ed4f748f7c doc-src/Tutorial/fp.tex
--- a/doc-src/Tutorial/fp.tex	Mon May 10 17:07:19 1999 +0200
+++ b/doc-src/Tutorial/fp.tex	Mon May 10 17:43:55 1999 +0200
@@ -358,7 +358,7 @@
 Lists are one of the essential datatypes in computing. Readers of this
 tutorial and users of HOL need to be familiar with their basic operations.
 Theory \texttt{ToyList} is only a small fragment of HOL's predefined theory
-\texttt{List}\footnote{\texttt{http://isabelle.in.tum.de/library/HOL/List.html}}.
+\texttt{List}\footnote{\url{http://isabelle.in.tum.de/library/HOL/List.html}}.
 The latter contains many further operations. For example, the functions
 \ttindexbold{hd} (`head') and \ttindexbold{tl} (`tail') return the first
 element and the remainder of a list. (However, pattern-matching is usually
diff -r c2511c9ea37e -r 12ed4f748f7c doc-src/Tutorial/tutorial.tex
--- a/doc-src/Tutorial/tutorial.tex	Mon May 10 17:07:19 1999 +0200
+++ b/doc-src/Tutorial/tutorial.tex	Mon May 10 17:43:55 1999 +0200
@@ -1,6 +1,6 @@
 \documentclass[11pt]{report}
-\usepackage{a4,latexsym,verbatim}
-\usepackage{graphicx}
+\usepackage{a4,latexsym,verbatim,graphicx,../pdfsetup}
+
 
 \makeatletter
 \input{../iman.sty}
@@ -39,13 +39,13 @@
 %\binperiod     %%%treat . like a binary operator
 
 \begin{document}
-\title{\includegraphics[scale=.8]{isabelle_hol.eps}
+\title{\includegraphics[scale=.8]{isabelle_hol}
        \\ \vspace{0.5cm} The Tutorial
        \\ --- DRAFT ---}
 \author{Tobias Nipkow\\
 Technische Universit\"at M\"unchen \\
 Institut f\"ur Informatik \\
-\texttt{http://www.in.tum.de/\~\relax nipkow/}}
+\url{http://www.in.tum.de/~nipkow/}}
 \maketitle
 
 \pagenumbering{roman}