diff -r f3ff2549cdc8 -r 23a118849801 doc-src/TutorialI/Misc/document/simp.tex --- 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}%