doc-src/TutorialI/preface.tex
changeset 12821 ed702a3af45c
parent 12813 f8f0807e5a5e
child 13141 f4ed10eaaff8
     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