diff -r d25be0ad1a6c -r 1b02a6c4032f doc-src/TutorialI/preface.tex
--- a/doc-src/TutorialI/preface.tex	Mon Jul 23 19:06:11 2001 +0200
+++ b/doc-src/TutorialI/preface.tex	Tue Jul 24 11:25:54 2001 +0200
@@ -8,8 +8,9 @@
 discussion of meta-theory.  It is written for potential users rather
 than for our colleagues in the research world.
 
-Another departure from previous documentation is the use of Markus
-Wenzel's proof script notation instead of ML tactic files.  The latter
+\index{Wenzel, Markus}%
+Another departure from previous documentation is that we describe Markus
+Wenzel's proof script notation instead of ML tactic scripts.  The latter
 make it easier to introduce new tactics on the fly, but hardly anybody
 does that.  Wenzel's dedicated syntax is elegant, replacing for example
 eight simplification tactics with a single method, namely \isa{simp},