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