diff -r bb01189f0565 -r 67cec35dbc58 doc-src/TutorialI/basics.tex
--- a/doc-src/TutorialI/basics.tex	Wed Mar 14 08:50:55 2001 +0100
+++ b/doc-src/TutorialI/basics.tex	Wed Mar 14 17:38:49 2001 +0100
@@ -17,12 +17,15 @@
 misled: HOL can express most mathematical concepts, and functional programming
 is just one particularly simple and ubiquitous instance.
 
-Isabelle~\cite{paulson-isa-book} is implemented in ML~\cite{SML}.
-This has influenced some of HOL's concrete syntax but is otherwise
-irrelevant for us because this tutorial is based on
-Isabelle/Isar~\cite{isabelle-isar-ref}, an extension of Isabelle
-with structured proofs.\footnote{Thus the full name of the system should be
-  Isabelle/Isar/HOL, but that is a bit of a mouthful.}
+Isabelle~\cite{paulson-isa-book} is implemented in ML~\cite{SML}.  This has
+influenced some of Isabelle/HOL's concrete syntax but is otherwise irrelevant
+for us because this tutorial is based on
+Isabelle/Isar~\cite{isabelle-isar-ref}, an extension of Isabelle with
+structured proofs. Thus the full name of the system should be
+Isabelle/Isar/HOL, but that is a bit of a mouthful. There are other
+implementations of HOL, in particular the one by Mike Gordon \emph{et al.},
+which is usually referred to as ``the HOL system'' \cite{mgordon-hol}. For us,
+HOL refers to the logical system, and sometimes its incarnation Isabelle/HOL.
 
 A tutorial is by definition incomplete.  Currently the tutorial only
 introduces the rudiments of Isar's proof language. To fully exploit the power