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




