# HG changeset patch
# User nipkow
# Date 1105173016 -3600
# Node ID b08a5eaf22e30087c5a9580eabf5fde2d2529826
# Parent  3f1a674b7ec714b2b164b78cf609b18859059135
new citation

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
diff -r 3f1a674b7ec7 -r b08a5eaf22e3 doc-src/manual.bib
--- 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}},