doc-src/TutorialI/Sets/Examples.thy
changeset 12815 1f073030b97a
parent 10864 f0b0a125ae4b
child 16417 9bc16273c2d4
     1.1 --- a/doc-src/TutorialI/Sets/Examples.thy	Fri Jan 18 17:46:17 2002 +0100
     1.2 +++ b/doc-src/TutorialI/Sets/Examples.thy	Fri Jan 18 18:30:19 2002 +0100
     1.3 @@ -90,7 +90,7 @@
     1.4  text{*A type constraint lets it work*}
     1.5  
     1.6  text{*An issue here: how do we discuss the distinction between ASCII and
     1.7 -X-symbol notation?  Here the latter disambiguates.*}
     1.8 +symbol notation?  Here the latter disambiguates.*}
     1.9  
    1.10  
    1.11  text{*