diff -r 2f5edb146f7e -r 1f073030b97a doc-src/TutorialI/Sets/Examples.thy
--- a/doc-src/TutorialI/Sets/Examples.thy	Fri Jan 18 17:46:17 2002 +0100
+++ b/doc-src/TutorialI/Sets/Examples.thy	Fri Jan 18 18:30:19 2002 +0100
@@ -90,7 +90,7 @@
 text{*A type constraint lets it work*}
 
 text{*An issue here: how do we discuss the distinction between ASCII and
-X-symbol notation?  Here the latter disambiguates.*}
+symbol notation?  Here the latter disambiguates.*}
 
 
 text{*