--- a/doc-src/TutorialI/Misc/document/simp.tex Thu Aug 09 10:17:45 2001 +0200
+++ b/doc-src/TutorialI/Misc/document/simp.tex Thu Aug 09 18:12:15 2001 +0200
@@ -287,7 +287,7 @@
\isa{case}-expressions, as it does \isa{if}-expressions,
because with recursive datatypes it could lead to nontermination.
Instead, the simplifier has a modifier
-\isa{split}\index{*split (modified)}
+\isa{split}\index{*split (modifier)}
for adding splitting rules explicitly. The
lemma above can be proved in one step by%
\end{isamarkuptxt}%