| changeset 19792 | e8e3da6d3ff7 |
| parent 16871 | 0f483b2632cd |
| child 20143 | 54e493016486 |
--- a/doc-src/TutorialI/Misc/simp.thy Tue Jun 06 15:02:55 2006 +0200 +++ b/doc-src/TutorialI/Misc/simp.thy Tue Jun 06 16:07:10 2006 +0200 @@ -330,7 +330,7 @@ text{* Polished proofs typically perform splitting within @{text simp} rather than invoking the @{text split} method. However, if a goal contains -several @{text if} and @{text case} expressions, +several @{text "if"} and @{text case} expressions, the @{text split} method can be helpful in selectively exploring the effects of splitting.