diff -r ab326de16ad5 -r e8e3da6d3ff7 doc-src/TutorialI/Misc/simp.thy
--- 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.