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