# HG changeset patch
# User nipkow
# Date 1011617056 -3600
# Node ID ed702a3af45c3c8163c0f0bc49cf4741c22b0f73
# Parent  02e2ff3e4d37baf091e48232b5c1792d0f22a41b
*** empty log message ***

diff -r 02e2ff3e4d37 -r ed702a3af45c doc-src/TutorialI/preface.tex
--- 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
diff -r 02e2ff3e4d37 -r ed702a3af45c doc-src/TutorialI/tutorial.ind
--- a/doc-src/TutorialI/tutorial.ind	Mon Jan 21 11:25:45 2002 +0100
+++ b/doc-src/TutorialI/tutorial.ind	Mon Jan 21 13:44:16 2002 +0100
@@ -647,7 +647,6 @@
 
   \indexspace
 
-  \item Wenzel, Markus, vii
   \item \isa {wf_induct} (theorem), \bold{115}
   \item \isa {wf_inv_image} (theorem), \bold{115}
   \item \isa {wf_less_than} (theorem), \bold{114}