1.1 --- a/doc-src/TutorialI/basics.tex	Thu Jan 06 05:15:26 2005 +0100
     1.2 +++ b/doc-src/TutorialI/basics.tex	Sat Jan 08 09:30:16 2005 +0100
     1.3 @@ -34,9 +34,10 @@
     1.4  A tutorial is by definition incomplete.  Currently the tutorial only
     1.5  introduces the rudiments of Isar's proof language. To fully exploit the power
     1.6  of Isar, in particular the ability to write readable and structured proofs,
     1.7 -you need to consult the Isabelle/Isar Reference
     1.8 -Manual~\cite{isabelle-isar-ref} and Wenzel's PhD thesis~\cite{Wenzel-PhD}
     1.9 -which discusses many proof patterns. If you want to use Isabelle's ML level
    1.10 +you should start with Nipkow's overview~\cite{Nipkow-TYPES02} and consult
    1.11 +the Isabelle/Isar Reference Manual~\cite{isabelle-isar-ref} and Wenzel's
    1.12 +PhD thesis~\cite{Wenzel-PhD} (which discusses many proof patterns)
    1.13 +for further details. If you want to use Isabelle's ML level
    1.14  directly (for example for writing your own proof procedures) see the Isabelle
    1.15  Reference Manual~\cite{isabelle-ref}; for details relating to HOL see the
    1.16  Isabelle/HOL manual~\cite{isabelle-HOL}. All manuals have a comprehensive