--- a/doc-src/TutorialI/preface.tex Mon Jan 21 11:25:45 2002 +0100
+++ b/doc-src/TutorialI/preface.tex Mon Jan 21 13:44:16 2002 +0100
@@ -9,7 +9,6 @@
discussion of meta-theory. It is written for potential users rather
than for our colleagues in the research world.
-\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