--- 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
--- a/doc-src/manual.bib Thu Jan 06 05:15:26 2005 +0100
+++ b/doc-src/manual.bib Sat Jan 08 09:30:16 2005 +0100
@@ -716,6 +716,17 @@
pages = {171-186},
year = 1998}
+@inproceedings{Nipkow-TYPES02,
+ author = {Tobias Nipkow},
+ title = {{Structured Proofs in Isar/HOL}},
+ booktitle = {Types for Proofs and Programs (TYPES 2002)},
+ editor = {H. Geuvers and F. Wiedijk},
+ year = 2003,
+ publisher = Springer,
+ series = LNCS,
+ volume = 2646,
+ pages = {259-278}}
+
@manual{isabelle-HOL,
author = {Tobias Nipkow and Lawrence C. Paulson and Markus Wenzel},
title = {{Isabelle}'s Logics: {HOL}},