| changeset 11494 | 23a118849801 |
| parent 11458 | 09a6c44a48ea |
| child 12332 | aea72a834c85 |
--- a/doc-src/TutorialI/Misc/simp.thy Thu Aug 09 10:17:45 2001 +0200 +++ b/doc-src/TutorialI/Misc/simp.thy Thu Aug 09 18:12:15 2001 +0200 @@ -281,7 +281,7 @@ @{text"case"}-expressions, as it does @{text"if"}-expressions, because with recursive datatypes it could lead to nontermination. Instead, the simplifier has a modifier -@{text split}\index{*split (modified)} +@{text split}\index{*split (modifier)} for adding splitting rules explicitly. The lemma above can be proved in one step by *}