1.1 --- a/doc-src/TutorialI/basics.tex	Mon Mar 19 10:37:47 2001 +0100
     1.2 +++ b/doc-src/TutorialI/basics.tex	Mon Mar 19 12:38:36 2001 +0100
     1.3 @@ -20,16 +20,19 @@
     1.4  Isabelle~\cite{paulson-isa-book} is implemented in ML~\cite{SML}.  This has
     1.5  influenced some of Isabelle/HOL's concrete syntax but is otherwise irrelevant
     1.6  for us because this tutorial is based on
     1.7 -Isabelle/Isar~\cite{isabelle-isar-ref}, an extension of Isabelle with
     1.8 -structured proofs. Thus the full name of the system should be
     1.9 -Isabelle/Isar/HOL, but that is a bit of a mouthful. There are other
    1.10 -implementations of HOL, in particular the one by Mike Gordon \emph{et al.},
    1.11 -which is usually referred to as ``the HOL system'' \cite{mgordon-hol}. For us,
    1.12 -HOL refers to the logical system, and sometimes its incarnation Isabelle/HOL.
    1.13 +Isabelle/Isar~\cite{isabelle-isar-ref}, an extension of Isabelle which hides
    1.14 +the implementation language almost completely.  Thus the full name of the
    1.15 +system should be Isabelle/Isar/HOL, but that is a bit of a mouthful.
    1.16 +
    1.17 +There are other implementations of HOL, in particular the one by Mike Gordon
    1.18 +\emph{et al.}, which is usually referred to as ``the HOL system''
    1.19 +\cite{mgordon-hol}. For us, HOL refers to the logical system, and sometimes
    1.20 +its incarnation Isabelle/HOL.
    1.21  
    1.22  A tutorial is by definition incomplete.  Currently the tutorial only
    1.23  introduces the rudiments of Isar's proof language. To fully exploit the power
    1.24 -of Isar you need to consult the Isabelle/Isar Reference
    1.25 +of Isar, in particular the ability to write readable and structured proofs,
    1.26 +you need to consult the Isabelle/Isar Reference
    1.27  Manual~\cite{isabelle-isar-ref}. If you want to use Isabelle's ML level
    1.28  directly (for example for writing your own proof procedures) see the Isabelle
    1.29  Reference Manual~\cite{isabelle-ref}; for details relating to HOL see the