doc-src/Tutorial/basics.tex
 changeset 6606 94b638b3827c parent 6584 5569f2672662 child 6628 12ed4f748f7c
--- a/doc-src/Tutorial/basics.tex	Thu May 06 11:13:01 1999 +0200
+++ b/doc-src/Tutorial/basics.tex	Thu May 06 11:48:09 1999 +0200
@@ -10,16 +10,15 @@
$\mbox{HOL} = \mbox{Functional Programming} + \mbox{Logic}.$
We assume that the reader is familiar with the basic concepts of both fields.
For excellent introductions to functional programming consult the textbooks
this tutorial initially concentrates on functional programming, do not be
misled: HOL can express most mathematical concepts, and functional
programming is just one particularly simple and ubiquitous instance.

A tutorial is by definition incomplete. To fully exploit the power of the
-system you need to consult the Isabelle Reference Manual~\cite{Isa-Ref-Man}
-for details about Isabelle and the HOL chapter of the Logics
-manual~\cite{Isa-Logics-Man} for details relating to HOL. Both manuals have a
-comprehensive index.
+system you need to consult the Isabelle Reference Manual~\cite{isabelle-ref}
+for details about Isabelle and the Isabelle/HOL manual~\cite{isabelle-HOL}
+for details relating to HOL. Both manuals have a comprehensive index.

\section{Theories, proofs and interaction}
\label{sec:Basic:Theories}
@@ -58,7 +57,7 @@
This tutorial is concerned with introducing you to the different linguistic
constructs that can fill ${\langle}declarations{\rangle}$ in the above theory template.
A complete grammar of the basic constructs is found in Appendix~A
-of~\cite{Isa-Ref-Man}, for reference in times of doubt.
+of~\cite{isabelle-ref}, for reference in times of doubt.

The tutorial is also concerned with showing you how to prove theorems about
the concepts in a theory. This involves invoking predefined theorem proving