1.1 --- a/doc-src/TutorialI/preface.tex Mon Jan 21 11:25:45 2002 +0100
1.2 +++ b/doc-src/TutorialI/preface.tex Mon Jan 21 13:44:16 2002 +0100
1.3 @@ -9,7 +9,6 @@
1.4 discussion of meta-theory. It is written for potential users rather
1.5 than for our colleagues in the research world.
1.6
1.7 -\index{Wenzel, Markus}%
1.8 Another departure from previous documentation is that we describe Markus
1.9 Wenzel's proof script notation instead of ML tactic scripts. The latter
1.10 make it easier to introduce new tactics on the fly, but hardly anybody