| changeset 12815 | 1f073030b97a |
| parent 10864 | f0b0a125ae4b |
| child 16417 | 9bc16273c2d4 |
--- 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{*