--- 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},